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 ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 B = A ↑ 𝑜 C ↔ B = C

Proof

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