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