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 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/CAFXXJSupG5Kf%2BNwsvy%3Dyqp2vNj6%3Dh9fNVhst3y4HOKPCHYQsNQ%40mail.gmail.com.
