I think the current way theorems about this are proved are using iundom <https://us.metamath.org/mpeuni/iundom.html> or iundom2g <https://us.metamath.org/mpeuni/iundom2g.html>. It's really about cardinalities of sets, but you can use this to infer well orderability (but not with an explicit ordering relation). If you need the actual relation this will need some refactoring.
On Thu, Aug 21, 2025 at 5:43 PM Mario Carneiro <[email protected]> wrote: > 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/CAFXXJSum73un0rXpxhLVRBSyrXfgEuwNg%3DWV3aKpzF%2BsBAh0qw%40mail.gmail.com.
