Metamath Proof Explorer

Theorem oeordi

Description: Ordering law for ordinal exponentiation. Proposition 8.33 of TakeutiZaring p. 67. (Contributed by NM, 5-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

Ref Expression
Assertion oeordi ⊢B∈On∧C∈On∖2𝑜→A∈B→C↑𝑜A∈C↑𝑜B

Proof

Step Hyp Ref Expression
1 oveq2 ⊢x=suc⁡A→C↑𝑜x=C↑𝑜suc⁡A
2 1 eleq2d ⊢x=suc⁡A→C↑𝑜A∈C↑𝑜x↔C↑𝑜A∈C↑𝑜suc⁡A
3 2 imbi2d ⊢x=suc⁡A→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜x↔C∈On∖2𝑜→C↑𝑜A∈C↑𝑜suc⁡A
4 oveq2 ⊢x=y→C↑𝑜x=C↑𝑜y
5 4 eleq2d ⊢x=y→C↑𝑜A∈C↑𝑜x↔C↑𝑜A∈C↑𝑜y
6 5 imbi2d ⊢x=y→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜x↔C∈On∖2𝑜→C↑𝑜A∈C↑𝑜y
7 oveq2 ⊢x=suc⁡y→C↑𝑜x=C↑𝑜suc⁡y
8 7 eleq2d ⊢x=suc⁡y→C↑𝑜A∈C↑𝑜x↔C↑𝑜A∈C↑𝑜suc⁡y
9 8 imbi2d ⊢x=suc⁡y→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜x↔C∈On∖2𝑜→C↑𝑜A∈C↑𝑜suc⁡y
10 oveq2 ⊢x=B→C↑𝑜x=C↑𝑜B
11 10 eleq2d ⊢x=B→C↑𝑜A∈C↑𝑜x↔C↑𝑜A∈C↑𝑜B
12 11 imbi2d ⊢x=B→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜x↔C∈On∖2𝑜→C↑𝑜A∈C↑𝑜B
13 eldifi ⊢C∈On∖2𝑜→C∈On
14 oecl ⊢C∈On∧A∈On→C↑𝑜A∈On
15 13 14 sylan ⊢C∈On∖2𝑜∧A∈On→C↑𝑜A∈On
16 om1 ⊢C↑𝑜A∈On→C↑𝑜A⋅𝑜1𝑜=C↑𝑜A
17 15 16 syl ⊢C∈On∖2𝑜∧A∈On→C↑𝑜A⋅𝑜1𝑜=C↑𝑜A
18 ondif2 ⊢C∈On∖2𝑜↔C∈On∧1𝑜∈C
19 18 simprbi ⊢C∈On∖2𝑜→1𝑜∈C
20 19 adantr ⊢C∈On∖2𝑜∧A∈On→1𝑜∈C
21 13 adantr ⊢C∈On∖2𝑜∧A∈On→C∈On
22 simpr ⊢C∈On∖2𝑜∧A∈On→A∈On
23 dif20el ⊢C∈On∖2𝑜→∅∈C
24 23 adantr ⊢C∈On∖2𝑜∧A∈On→∅∈C
25 oen0 ⊢C∈On∧A∈On∧∅∈C→∅∈C↑𝑜A
26 21 22 24 25 syl21anc ⊢C∈On∖2𝑜∧A∈On→∅∈C↑𝑜A
27 omordi ⊢C∈On∧C↑𝑜A∈On∧∅∈C↑𝑜A→1𝑜∈C→C↑𝑜A⋅𝑜1𝑜∈C↑𝑜A⋅𝑜C
28 21 15 26 27 syl21anc ⊢C∈On∖2𝑜∧A∈On→1𝑜∈C→C↑𝑜A⋅𝑜1𝑜∈C↑𝑜A⋅𝑜C
29 20 28 mpd ⊢C∈On∖2𝑜∧A∈On→C↑𝑜A⋅𝑜1𝑜∈C↑𝑜A⋅𝑜C
30 17 29 eqeltrrd ⊢C∈On∖2𝑜∧A∈On→C↑𝑜A∈C↑𝑜A⋅𝑜C
31 oesuc ⊢C∈On∧A∈On→C↑𝑜suc⁡A=C↑𝑜A⋅𝑜C
32 13 31 sylan ⊢C∈On∖2𝑜∧A∈On→C↑𝑜suc⁡A=C↑𝑜A⋅𝑜C
33 30 32 eleqtrrd ⊢C∈On∖2𝑜∧A∈On→C↑𝑜A∈C↑𝑜suc⁡A
34 33 expcom ⊢A∈On→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜suc⁡A
35 oecl ⊢C∈On∧y∈On→C↑𝑜y∈On
36 13 35 sylan ⊢C∈On∖2𝑜∧y∈On→C↑𝑜y∈On
37 om1 ⊢C↑𝑜y∈On→C↑𝑜y⋅𝑜1𝑜=C↑𝑜y
38 36 37 syl ⊢C∈On∖2𝑜∧y∈On→C↑𝑜y⋅𝑜1𝑜=C↑𝑜y
39 19 adantr ⊢C∈On∖2𝑜∧y∈On→1𝑜∈C
40 13 adantr ⊢C∈On∖2𝑜∧y∈On→C∈On
41 simpr ⊢C∈On∖2𝑜∧y∈On→y∈On
42 23 adantr ⊢C∈On∖2𝑜∧y∈On→∅∈C
43 oen0 ⊢C∈On∧y∈On∧∅∈C→∅∈C↑𝑜y
44 40 41 42 43 syl21anc ⊢C∈On∖2𝑜∧y∈On→∅∈C↑𝑜y
45 omordi ⊢C∈On∧C↑𝑜y∈On∧∅∈C↑𝑜y→1𝑜∈C→C↑𝑜y⋅𝑜1𝑜∈C↑𝑜y⋅𝑜C
46 40 36 44 45 syl21anc ⊢C∈On∖2𝑜∧y∈On→1𝑜∈C→C↑𝑜y⋅𝑜1𝑜∈C↑𝑜y⋅𝑜C
47 39 46 mpd ⊢C∈On∖2𝑜∧y∈On→C↑𝑜y⋅𝑜1𝑜∈C↑𝑜y⋅𝑜C
48 38 47 eqeltrrd ⊢C∈On∖2𝑜∧y∈On→C↑𝑜y∈C↑𝑜y⋅𝑜C
49 oesuc ⊢C∈On∧y∈On→C↑𝑜suc⁡y=C↑𝑜y⋅𝑜C
50 13 49 sylan ⊢C∈On∖2𝑜∧y∈On→C↑𝑜suc⁡y=C↑𝑜y⋅𝑜C
51 48 50 eleqtrrd ⊢C∈On∖2𝑜∧y∈On→C↑𝑜y∈C↑𝑜suc⁡y
52 onsuc ⊢y∈On→suc⁡y∈On
53 oecl ⊢C∈On∧suc⁡y∈On→C↑𝑜suc⁡y∈On
54 13 52 53 syl2an ⊢C∈On∖2𝑜∧y∈On→C↑𝑜suc⁡y∈On
55 ontr1 ⊢C↑𝑜suc⁡y∈On→C↑𝑜A∈C↑𝑜y∧C↑𝑜y∈C↑𝑜suc⁡y→C↑𝑜A∈C↑𝑜suc⁡y
56 54 55 syl ⊢C∈On∖2𝑜∧y∈On→C↑𝑜A∈C↑𝑜y∧C↑𝑜y∈C↑𝑜suc⁡y→C↑𝑜A∈C↑𝑜suc⁡y
57 51 56 mpan2d ⊢C∈On∖2𝑜∧y∈On→C↑𝑜A∈C↑𝑜y→C↑𝑜A∈C↑𝑜suc⁡y
58 57 expcom ⊢y∈On→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜y→C↑𝑜A∈C↑𝑜suc⁡y
59 58 adantr ⊢y∈On∧A∈y→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜y→C↑𝑜A∈C↑𝑜suc⁡y
60 59 a2d ⊢y∈On∧A∈y→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜y→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜suc⁡y
61 bi2.04 ⊢A∈y→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜y↔C∈On∖2𝑜→A∈y→C↑𝑜A∈C↑𝑜y
62 61 ralbii ⊢∀y∈xA∈y→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜y↔∀y∈xC∈On∖2𝑜→A∈y→C↑𝑜A∈C↑𝑜y
63 r19.21v ⊢∀y∈xC∈On∖2𝑜→A∈y→C↑𝑜A∈C↑𝑜y↔C∈On∖2𝑜→∀y∈xA∈y→C↑𝑜A∈C↑𝑜y
64 62 63 bitri ⊢∀y∈xA∈y→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜y↔C∈On∖2𝑜→∀y∈xA∈y→C↑𝑜A∈C↑𝑜y
65 limsuc ⊢Lim⁡x→A∈x↔suc⁡A∈x
66 65 biimpa ⊢Lim⁡x∧A∈x→suc⁡A∈x
67 elex ⊢suc⁡A∈x→suc⁡A∈V
68 sucexb ⊢A∈V↔suc⁡A∈V
69 sucidg ⊢A∈V→A∈suc⁡A
70 68 69 sylbir ⊢suc⁡A∈V→A∈suc⁡A
71 67 70 syl ⊢suc⁡A∈x→A∈suc⁡A
72 eleq2 ⊢y=suc⁡A→A∈y↔A∈suc⁡A
73 oveq2 ⊢y=suc⁡A→C↑𝑜y=C↑𝑜suc⁡A
74 73 eleq2d ⊢y=suc⁡A→C↑𝑜A∈C↑𝑜y↔C↑𝑜A∈C↑𝑜suc⁡A
75 72 74 imbi12d ⊢y=suc⁡A→A∈y→C↑𝑜A∈C↑𝑜y↔A∈suc⁡A→C↑𝑜A∈C↑𝑜suc⁡A
76 75 rspcv ⊢suc⁡A∈x→∀y∈xA∈y→C↑𝑜A∈C↑𝑜y→A∈suc⁡A→C↑𝑜A∈C↑𝑜suc⁡A
77 71 76 mpid ⊢suc⁡A∈x→∀y∈xA∈y→C↑𝑜A∈C↑𝑜y→C↑𝑜A∈C↑𝑜suc⁡A
78 77 anc2li ⊢suc⁡A∈x→∀y∈xA∈y→C↑𝑜A∈C↑𝑜y→suc⁡A∈x∧C↑𝑜A∈C↑𝑜suc⁡A
79 73 eliuni ⊢suc⁡A∈x∧C↑𝑜A∈C↑𝑜suc⁡A→C↑𝑜A∈⋃y∈xC↑𝑜y
80 78 79 syl6 ⊢suc⁡A∈x→∀y∈xA∈y→C↑𝑜A∈C↑𝑜y→C↑𝑜A∈⋃y∈xC↑𝑜y
81 66 80 syl ⊢Lim⁡x∧A∈x→∀y∈xA∈y→C↑𝑜A∈C↑𝑜y→C↑𝑜A∈⋃y∈xC↑𝑜y
82 81 adantr ⊢Lim⁡x∧A∈x∧C∈On∖2𝑜→∀y∈xA∈y→C↑𝑜A∈C↑𝑜y→C↑𝑜A∈⋃y∈xC↑𝑜y
83 13 adantl ⊢Lim⁡x∧C∈On∖2𝑜→C∈On
84 simpl ⊢Lim⁡x∧C∈On∖2𝑜→Lim⁡x
85 23 adantl ⊢Lim⁡x∧C∈On∖2𝑜→∅∈C
86 vex ⊢x∈V
87 oelim ⊢C∈On∧x∈V∧Lim⁡x∧∅∈C→C↑𝑜x=⋃y∈xC↑𝑜y
88 86 87 mpanlr1 ⊢C∈On∧Lim⁡x∧∅∈C→C↑𝑜x=⋃y∈xC↑𝑜y
89 83 84 85 88 syl21anc ⊢Lim⁡x∧C∈On∖2𝑜→C↑𝑜x=⋃y∈xC↑𝑜y
90 89 adantlr ⊢Lim⁡x∧A∈x∧C∈On∖2𝑜→C↑𝑜x=⋃y∈xC↑𝑜y
91 90 eleq2d ⊢Lim⁡x∧A∈x∧C∈On∖2𝑜→C↑𝑜A∈C↑𝑜x↔C↑𝑜A∈⋃y∈xC↑𝑜y
92 82 91 sylibrd ⊢Lim⁡x∧A∈x∧C∈On∖2𝑜→∀y∈xA∈y→C↑𝑜A∈C↑𝑜y→C↑𝑜A∈C↑𝑜x
93 92 ex ⊢Lim⁡x∧A∈x→C∈On∖2𝑜→∀y∈xA∈y→C↑𝑜A∈C↑𝑜y→C↑𝑜A∈C↑𝑜x
94 93 a2d ⊢Lim⁡x∧A∈x→C∈On∖2𝑜→∀y∈xA∈y→C↑𝑜A∈C↑𝑜y→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜x
95 64 94 biimtrid ⊢Lim⁡x∧A∈x→∀y∈xA∈y→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜y→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜x
96 3 6 9 12 34 60 95 tfindsg2 ⊢B∈On∧A∈B→C∈On∖2𝑜→C↑𝑜A∈C↑𝑜B
97 96 impancom ⊢B∈On∧C∈On∖2𝑜→A∈B→C↑𝑜A∈C↑𝑜B