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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 +o 𝐵 ) = ( 𝐴 +o 𝐶 ) ↔ 𝐵 = 𝐶 ) )

Proof

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