My immediate reaction is that something like this proof must exist in order to establish the facts about tarski universes being well orderable and the relationship between tarski and grothendieck universes. Not sure if it will exist in the explicit form you have here though, where you have chosen well orders and want an explicit well order on the union, rather than simply knowing it is well orderable.
On Thu, Aug 21, 2025 at 5:40 PM Matthew House <[email protected]> wrote: > For a proof by Jech related to AC implications, I've been looking for a > theorem along the lines of > > $e T = { <. y , z >. | ... } $. > $p |- ( ( R We A /\ R Se A /\ A. x e. A S We B ) -> T We U_ x e. A B ) $. > > (S and B are to be read as S(x) and B(x). Also, a version with more > sethood hypotheses would also be acceptable, since my specific use case is > along the lines of ( ( A e. On /\ A. x e. A ( f ` x ) We ( g ` x ) ) -> > U_ x e. A ( g ` x ) e. dom card ).) > > Intuitively, the idea for proving it is relatively simple (Jech elides it > with an "easily"): Given y and z, we first compare the R-minimal x such > that y e. B(x) with the R-minimal x' such that z e. B(x'); if x = x', > then we can fall back to comparing with S(x). In other words, we line up > all the B(x)s in order of their xs, then sort by S(x) within each B(x). > > It's also pretty simple to write out a T implementing this procedure, but > working out the proof has me stumped. I tried directly working out the > conditions for T Fr U_ x e. A B and T Or U_ x e. A B, but I got lost in > extremely long lines of iota_ soup. So I looked into the existing > theorems for well-orders, but they don't seem helpful. fnwe > <https://us.metamath.org/mpeuni/fnwe.html> looked somewhat nice, except > that it requires a single S relation, which would be very messy to paste > together. Another idea was to use an injection from U_ x e. A B to <. A , > U_ x e. A B >. with a lexicographical well-order, but wexp > <https://us.metamath.org/mpeuni/wexp.html> & co. would similarly require > the S relations to be pasted together. > > Is there some clever way of proving this with existing theorems, or will I > have to do this the hard way? > > Thank you, > Matthew House > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/metamath/c6ea2730-ed64-4464-9dfb-9c1cc173654an%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/c6ea2730-ed64-4464-9dfb-9c1cc173654an%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSsdW84yvWNC2TSqDFz-Eu7wToksGk7AtT%2BgZaaXam%3DBjw%40mail.gmail.com.
