Metamath Proof Explorer

Theorem oeord

Description: Ordering property of ordinal exponentiation. Corollary 8.34 of TakeutiZaring p. 68 and its converse. (Contributed by NM, 6-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

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

Proof

Step Hyp Ref Expression
1 oeordi ⊢ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ∈ B → C ↑ 𝑜 A ∈ C ↑ 𝑜 B
2 1 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ∈ B → C ↑ 𝑜 A ∈ C ↑ 𝑜 B
3 oveq2 ⊢ A = B → C ↑ 𝑜 A = C ↑ 𝑜 B
4 3 a1i ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A = B → C ↑ 𝑜 A = C ↑ 𝑜 B
5 oeordi ⊢ A ∈ On ∧ C ∈ On ∖ 2 𝑜 → B ∈ A → C ↑ 𝑜 B ∈ C ↑ 𝑜 A
6 5 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → B ∈ A → C ↑ 𝑜 B ∈ C ↑ 𝑜 A
7 4 6 orim12d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A = B ∨ B ∈ A → C ↑ 𝑜 A = C ↑ 𝑜 B ∨ C ↑ 𝑜 B ∈ C ↑ 𝑜 A
8 7 con3d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → ¬ C ↑ 𝑜 A = C ↑ 𝑜 B ∨ C ↑ 𝑜 B ∈ C ↑ 𝑜 A → ¬ A = B ∨ B ∈ A
9 eldifi ⊢ C ∈ On ∖ 2 𝑜 → C ∈ On
10 9 3ad2ant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → C ∈ On
11 simp1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ∈ On
12 oecl ⊢ C ∈ On ∧ A ∈ On → C ↑ 𝑜 A ∈ On
13 10 11 12 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 A ∈ On
14 simp2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → B ∈ On
15 oecl ⊢ C ∈ On ∧ B ∈ On → C ↑ 𝑜 B ∈ On
16 10 14 15 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 B ∈ On
17 eloni ⊢ C ↑ 𝑜 A ∈ On → Ord ⁡ C ↑ 𝑜 A
18 eloni ⊢ C ↑ 𝑜 B ∈ On → Ord ⁡ C ↑ 𝑜 B
19 ordtri2 ⊢ Ord ⁡ C ↑ 𝑜 A ∧ Ord ⁡ C ↑ 𝑜 B → C ↑ 𝑜 A ∈ C ↑ 𝑜 B ↔ ¬ C ↑ 𝑜 A = C ↑ 𝑜 B ∨ C ↑ 𝑜 B ∈ C ↑ 𝑜 A
20 17 18 19 syl2an ⊢ C ↑ 𝑜 A ∈ On ∧ C ↑ 𝑜 B ∈ On → C ↑ 𝑜 A ∈ C ↑ 𝑜 B ↔ ¬ C ↑ 𝑜 A = C ↑ 𝑜 B ∨ C ↑ 𝑜 B ∈ C ↑ 𝑜 A
21 13 16 20 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 A ∈ C ↑ 𝑜 B ↔ ¬ C ↑ 𝑜 A = C ↑ 𝑜 B ∨ C ↑ 𝑜 B ∈ C ↑ 𝑜 A
22 eloni ⊢ A ∈ On → Ord ⁡ A
23 eloni ⊢ B ∈ On → Ord ⁡ B
24 ordtri2 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ↔ ¬ A = B ∨ B ∈ A
25 22 23 24 syl2an ⊢ A ∈ On ∧ B ∈ On → A ∈ B ↔ ¬ A = B ∨ B ∈ A
26 25 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ∈ B ↔ ¬ A = B ∨ B ∈ A
27 8 21 26 3imtr4d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 A ∈ C ↑ 𝑜 B → A ∈ B
28 2 27 impbid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ∈ B ↔ C ↑ 𝑜 A ∈ C ↑ 𝑜 B