Metamath Proof Explorer

Theorem oecan

Description: Left cancellation law for ordinal exponentiation. (Contributed by NM, 6-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

Ref Expression
Assertion oecan ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o 𝐵 ) = ( 𝐴 ↑o 𝐶 ) ↔ 𝐵 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 oeordi ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ↑o 𝐵 ) ∈ ( 𝐴 ↑o 𝐶 ) ) )
2 1 ancoms ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ↑o 𝐵 ) ∈ ( 𝐴 ↑o 𝐶 ) ) )
3 2 3adant2 ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ↑o 𝐵 ) ∈ ( 𝐴 ↑o 𝐶 ) ) )
4 oeordi ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝐶 ∈ 𝐵 → ( 𝐴 ↑o 𝐶 ) ∈ ( 𝐴 ↑o 𝐵 ) ) )
5 4 ancoms ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( 𝐶 ∈ 𝐵 → ( 𝐴 ↑o 𝐶 ) ∈ ( 𝐴 ↑o 𝐵 ) ) )
6 5 3adant3 ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 ∈ 𝐵 → ( 𝐴 ↑o 𝐶 ) ∈ ( 𝐴 ↑o 𝐵 ) ) )
7 3 6 orim12d ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) → ( ( 𝐴 ↑o 𝐵 ) ∈ ( 𝐴 ↑o 𝐶 ) ∨ ( 𝐴 ↑o 𝐶 ) ∈ ( 𝐴 ↑o 𝐵 ) ) ) )
8 7 con3d ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ¬ ( ( 𝐴 ↑o 𝐵 ) ∈ ( 𝐴 ↑o 𝐶 ) ∨ ( 𝐴 ↑o 𝐶 ) ∈ ( 𝐴 ↑o 𝐵 ) ) → ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
9 eldifi ⊢ ( 𝐴 ∈ ( On ∖ 2o ) → 𝐴 ∈ On )
10 9 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐴 ∈ On )
11 simp2 ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐵 ∈ On )
12 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
13 10 11 12 syl2anc ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
14 simp3 ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐶 ∈ On )
15 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o 𝐶 ) ∈ On )
16 10 14 15 syl2anc ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o 𝐶 ) ∈ On )
17 eloni ⊢ ( ( 𝐴 ↑o 𝐵 ) ∈ On → Ord ( 𝐴 ↑o 𝐵 ) )
18 eloni ⊢ ( ( 𝐴 ↑o 𝐶 ) ∈ On → Ord ( 𝐴 ↑o 𝐶 ) )
19 ordtri3 ⊢ ( ( 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 ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o 𝐵 ) = ( 𝐴 ↑o 𝐶 ) ↔ ¬ ( ( 𝐴 ↑o 𝐵 ) ∈ ( 𝐴 ↑o 𝐶 ) ∨ ( 𝐴 ↑o 𝐶 ) ∈ ( 𝐴 ↑o 𝐵 ) ) ) )
22 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
23 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
24 ordtri3 ⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
25 22 23 24 syl2an ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
26 25 3adant1 ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
27 8 21 26 3imtr4d ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o 𝐵 ) = ( 𝐴 ↑o 𝐶 ) → 𝐵 = 𝐶 ) )
28 oveq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐴 ↑o 𝐵 ) = ( 𝐴 ↑o 𝐶 ) )
29 27 28 impbid1 ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o 𝐵 ) = ( 𝐴 ↑o 𝐶 ) ↔ 𝐵 = 𝐶 ) )