Metamath Proof Explorer


Theorem ondomon

Description: The class of ordinals dominated by a given set is an ordinal. Theorem 56 of Suppes p. 227. This theorem can be proved without the axiom of choice, see hartogs . (Contributed by NM, 7-Nov-2003) (Proof modification is discouraged.) Use hartogs instead. (New usage is discouraged.)

Ref Expression
Assertion ondomon AVxOn|xAOn

Proof

Step Hyp Ref Expression
1 onelon zOnyzyOn
2 vex zV
3 onelss zOnyzyz
4 3 imp zOnyzyz
5 ssdomg zVyzyz
6 2 4 5 mpsyl zOnyzyz
7 1 6 jca zOnyzyOnyz
8 domtr yzzAyA
9 8 anim2i yOnyzzAyOnyA
10 9 anassrs yOnyzzAyOnyA
11 7 10 sylan zOnyzzAyOnyA
12 11 exp31 zOnyzzAyOnyA
13 12 com12 yzzOnzAyOnyA
14 13 impd yzzOnzAyOnyA
15 breq1 x=zxAzA
16 15 elrab zxOn|xAzOnzA
17 breq1 x=yxAyA
18 17 elrab yxOn|xAyOnyA
19 14 16 18 3imtr4g yzzxOn|xAyxOn|xA
20 19 imp yzzxOn|xAyxOn|xA
21 20 gen2 yzyzzxOn|xAyxOn|xA
22 dftr2 TrxOn|xAyzyzzxOn|xAyxOn|xA
23 21 22 mpbir TrxOn|xA
24 ssrab2 xOn|xAOn
25 ordon OrdOn
26 trssord TrxOn|xAxOn|xAOnOrdOnOrdxOn|xA
27 23 24 25 26 mp3an OrdxOn|xA
28 elex AVAV
29 canth2g AVA𝒫A
30 domsdomtr xAA𝒫Ax𝒫A
31 29 30 sylan2 xAAVx𝒫A
32 31 expcom AVxAx𝒫A
33 32 ralrimivw AVxOnxAx𝒫A
34 28 33 syl AVxOnxAx𝒫A
35 ss2rab xOn|xAxOn|x𝒫AxOnxAx𝒫A
36 34 35 sylibr AVxOn|xAxOn|x𝒫A
37 pwexg AV𝒫AV
38 numth3 𝒫AV𝒫Adomcard
39 cardval2 𝒫Adomcardcard𝒫A=xOn|x𝒫A
40 37 38 39 3syl AVcard𝒫A=xOn|x𝒫A
41 fvex card𝒫AV
42 40 41 eqeltrrdi AVxOn|x𝒫AV
43 ssexg xOn|xAxOn|x𝒫AxOn|x𝒫AVxOn|xAV
44 36 42 43 syl2anc AVxOn|xAV
45 elong xOn|xAVxOn|xAOnOrdxOn|xA
46 44 45 syl AVxOn|xAOnOrdxOn|xA
47 27 46 mpbiri AVxOn|xAOn