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