Ah, now that's a clever way of doing it, thank you! I'll have to keep that in mind, that passing to ordinals is an easy way of simplifying indexed unions. Though the choice hypothesis |- ( ph -> U_ x e. A ( C ^m B ) e. AC_ A ) for iundomg <https://us.metamath.org/mpeuni/iundomg.html> is a bit annoying, even if I can satisfy it in my particular use case. Also, I'd already gotten most of the way through the *tour de force* of a direct proof, so I decided to finish it and post the theorems at #4989 <https://github.com/metamath/set.mm/pull/4989>.
On Sat, Aug 23, 2025 at 5:19 AM Mario Carneiro <[email protected]> wrote: > If you are after U_ x e. A B rather than U_ x e. A ( { x } X. B ) then I > think you want to use iundom(g) instead of iundom2g (which is about > disjoint union). If you know that each B(x) is well orderable, then B(x) ~~ > (card`B(x)) (cardid2 <https://us.metamath.org/mpeuni/cardid2.html>), so > U_ x e. A (card`B(x)) is an ordinal which is larger than every B(x). You > can use this in iundom as the upper bound, to prove that U_ x e. A B is > also well orderable using numdom > <https://us.metamath.org/mpeuni/numdom.html>. > > On Thu, Aug 21, 2025 at 7:51 PM Matthew House <[email protected]> > wrote: > >> 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 >> <https://groups.google.com/d/msgid/metamath/892e7429-0fef-45c8-b72f-cf999214b1a4n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- > You received this message because you are subscribed to a topic in the > Google Groups "Metamath" group. > To unsubscribe from this topic, visit > https://groups.google.com/d/topic/metamath/AQHekL6oEsA/unsubscribe. > To unsubscribe from this group and all its topics, send an email to > [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/metamath/CAFXXJSupG5Kf%2BNwsvy%3Dyqp2vNj6%3Dh9fNVhst3y4HOKPCHYQsNQ%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJSupG5Kf%2BNwsvy%3Dyqp2vNj6%3Dh9fNVhst3y4HOKPCHYQsNQ%40mail.gmail.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/CADBQv9bD1XNMvx1400ud-rE4dOMODGF3Os3SxZmo8q6h5byCNg%40mail.gmail.com.
