Thank you, iundom2g <https://us.metamath.org/mpeuni/iundom2g.html> looks closer like what I'm looking for. In this case, I ultimately only need U_ x e. A B e. dom card. But how could I get to there from iundom2g's cardinality conclusion? The simple application of U_ x e. A ( { x } X. B ) ~<_ ( A X. U_ x e. A B ) doesn't seem to help much without ( A X. U_ x e. A B ) e. dom card, which would seemingly have the same problem of having to paste together the Ss.
On Thursday, August 21, 2025 at 12:11:07 PM UTC-4 [email protected] wrote: > 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/892e7429-0fef-45c8-b72f-cf999214b1a4n%40googlegroups.com.
