Metamath Proof Explorer

Theorem oacan

Description: Left cancellation law for ordinal addition. Corollary 8.5 of TakeutiZaring p. 58. (Contributed by NM, 5-Dec-2004)

Ref Expression
Assertion oacan ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + 𝑜 B = A + 𝑜 C ↔ B = C

Proof

Step Hyp Ref Expression
1 oaord ⊢ B ∈ On ∧ C ∈ On ∧ A ∈ On → B ∈ C ↔ A + 𝑜 B ∈ A + 𝑜 C
2 1 3comr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ∈ C ↔ A + 𝑜 B ∈ A + 𝑜 C
3 oaord ⊢ C ∈ On ∧ B ∈ On ∧ A ∈ On → C ∈ B ↔ A + 𝑜 C ∈ A + 𝑜 B
4 3 3com13 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ∈ B ↔ A + 𝑜 C ∈ A + 𝑜 B
5 2 4 orbi12d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ∈ C ∨ C ∈ B ↔ A + 𝑜 B ∈ A + 𝑜 C ∨ A + 𝑜 C ∈ A + 𝑜 B
6 5 notbid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ¬ B ∈ C ∨ C ∈ B ↔ ¬ A + 𝑜 B ∈ A + 𝑜 C ∨ A + 𝑜 C ∈ A + 𝑜 B
7 eloni ⊢ B ∈ On → Ord ⁡ B
8 eloni ⊢ C ∈ On → Ord ⁡ C
9 ordtri3 ⊢ Ord ⁡ B ∧ Ord ⁡ C → B = C ↔ ¬ B ∈ C ∨ C ∈ B
10 7 8 9 syl2an ⊢ B ∈ On ∧ C ∈ On → B = C ↔ ¬ B ∈ C ∨ C ∈ B
11 10 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B = C ↔ ¬ B ∈ C ∨ C ∈ B
12 oacl ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ∈ On
13 eloni ⊢ A + 𝑜 B ∈ On → Ord ⁡ A + 𝑜 B
14 12 13 syl ⊢ A ∈ On ∧ B ∈ On → Ord ⁡ A + 𝑜 B
15 oacl ⊢ A ∈ On ∧ C ∈ On → A + 𝑜 C ∈ On
16 eloni ⊢ A + 𝑜 C ∈ On → Ord ⁡ A + 𝑜 C
17 15 16 syl ⊢ A ∈ On ∧ C ∈ On → Ord ⁡ A + 𝑜 C
18 ordtri3 ⊢ Ord ⁡ A + 𝑜 B ∧ Ord ⁡ A + 𝑜 C → A + 𝑜 B = A + 𝑜 C ↔ ¬ A + 𝑜 B ∈ A + 𝑜 C ∨ A + 𝑜 C ∈ A + 𝑜 B
19 14 17 18 syl2an ⊢ A ∈ On ∧ B ∈ On ∧ A ∈ On ∧ C ∈ On → A + 𝑜 B = A + 𝑜 C ↔ ¬ A + 𝑜 B ∈ A + 𝑜 C ∨ A + 𝑜 C ∈ A + 𝑜 B
20 19 3impdi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + 𝑜 B = A + 𝑜 C ↔ ¬ A + 𝑜 B ∈ A + 𝑜 C ∨ A + 𝑜 C ∈ A + 𝑜 B
21 6 11 20 3bitr4rd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + 𝑜 B = A + 𝑜 C ↔ B = C