This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ) )

Proof

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