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 suceloni ⊢ 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 ∈ x A ∈ y → C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 A ∈ C ↑ 𝑜 y ↔ ∀ y ∈ x C ∈ On ∖ 2 𝑜 → A ∈ y → C ↑ 𝑜 A ∈ C ↑ 𝑜 y
63 r19.21v ⊢ ∀ y ∈ x C ∈ On ∖ 2 𝑜 → A ∈ y → C ↑ 𝑜 A ∈ C ↑ 𝑜 y ↔ C ∈ On ∖ 2 𝑜 → ∀ y ∈ x A ∈ y → C ↑ 𝑜 A ∈ C ↑ 𝑜 y
64 62 63 bitri ⊢ ∀ y ∈ x A ∈ y → C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 A ∈ C ↑ 𝑜 y ↔ C ∈ On ∖ 2 𝑜 → ∀ y ∈ x A ∈ 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 ∈ x A ∈ y → C ↑ 𝑜 A ∈ C ↑ 𝑜 y → A ∈ suc ⁡ A → C ↑ 𝑜 A ∈ C ↑ 𝑜 suc ⁡ A
77 71 76 mpid ⊢ suc ⁡ A ∈ x → ∀ y ∈ x A ∈ y → C ↑ 𝑜 A ∈ C ↑ 𝑜 y → C ↑ 𝑜 A ∈ C ↑ 𝑜 suc ⁡ A
78 77 anc2li ⊢ suc ⁡ A ∈ x → ∀ y ∈ x A ∈ 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 ∈ x C ↑ 𝑜 y
80 78 79 syl6 ⊢ suc ⁡ A ∈ x → ∀ y ∈ x A ∈ y → C ↑ 𝑜 A ∈ C ↑ 𝑜 y → C ↑ 𝑜 A ∈ ⋃ y ∈ x C ↑ 𝑜 y
81 66 80 syl ⊢ Lim ⁡ x ∧ A ∈ x → ∀ y ∈ x A ∈ y → C ↑ 𝑜 A ∈ C ↑ 𝑜 y → C ↑ 𝑜 A ∈ ⋃ y ∈ x C ↑ 𝑜 y
82 81 adantr ⊢ Lim ⁡ x ∧ A ∈ x ∧ C ∈ On ∖ 2 𝑜 → ∀ y ∈ x A ∈ y → C ↑ 𝑜 A ∈ C ↑ 𝑜 y → C ↑ 𝑜 A ∈ ⋃ y ∈ x C ↑ 𝑜 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 ∈ x C ↑ 𝑜 y
88 86 87 mpanlr1 ⊢ C ∈ On ∧ Lim ⁡ x ∧ ∅ ∈ C → C ↑ 𝑜 x = ⋃ y ∈ x C ↑ 𝑜 y
89 83 84 85 88 syl21anc ⊢ Lim ⁡ x ∧ C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 x = ⋃ y ∈ x C ↑ 𝑜 y
90 89 adantlr ⊢ Lim ⁡ x ∧ A ∈ x ∧ C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 x = ⋃ y ∈ x C ↑ 𝑜 y
91 90 eleq2d ⊢ Lim ⁡ x ∧ A ∈ x ∧ C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 A ∈ C ↑ 𝑜 x ↔ C ↑ 𝑜 A ∈ ⋃ y ∈ x C ↑ 𝑜 y
92 82 91 sylibrd ⊢ Lim ⁡ x ∧ A ∈ x ∧ C ∈ On ∖ 2 𝑜 → ∀ y ∈ x A ∈ y → C ↑ 𝑜 A ∈ C ↑ 𝑜 y → C ↑ 𝑜 A ∈ C ↑ 𝑜 x
93 92 ex ⊢ Lim ⁡ x ∧ A ∈ x → C ∈ On ∖ 2 𝑜 → ∀ y ∈ x A ∈ y → C ↑ 𝑜 A ∈ C ↑ 𝑜 y → C ↑ 𝑜 A ∈ C ↑ 𝑜 x
94 93 a2d ⊢ Lim ⁡ x ∧ A ∈ x → C ∈ On ∖ 2 𝑜 → ∀ y ∈ x A ∈ y → C ↑ 𝑜 A ∈ C ↑ 𝑜 y → C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 A ∈ C ↑ 𝑜 x
95 64 94 syl5bi ⊢ Lim ⁡ x ∧ A ∈ x → ∀ y ∈ x A ∈ 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