Constructing a well-order from a family of well-orders?

[Matthew House]

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 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 & 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

[Mario Carneiro]

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.

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/c6ea2730-ed64-4464-9dfb-9c1cc173654an%40googlegroups.com.

[Mario Carneiro]

I think the current way theorems about this are proved are using iundom or iundom2g. 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.

[Matthew House]

Thank you, iundom2g 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.

[Mario Carneiro]

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), 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.

To view this discussion visit https://groups.google.com/d/msgid/metamath/892e7429-0fef-45c8-b72f-cf999214b1a4n%40googlegroups.com.

[Matthew House]

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 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.

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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSupG5Kf%2BNwsvy%3Dyqp2vNj6%3Dh9fNVhst3y4HOKPCHYQsNQ%40mail.gmail.com.