This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omcan

Description: Left cancellation law for ordinal multiplication. Proposition 8.20 of TakeutiZaring p. 63 and its converse. (Contributed by NM, 14-Dec-2004)

Ref Expression
Assertion omcan ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) ↔ 𝐵 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 omordi ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )
2 1 ex ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) ) )
3 2 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) ) )
4 3 3adant2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) ) )
5 4 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )
6 omordi ⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐶 ∈ 𝐵 → ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) )
7 6 ex ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐶 ∈ 𝐵 → ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
8 7 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐶 ∈ 𝐵 → ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
9 8 3adant3 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐶 ∈ 𝐵 → ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
10 9 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐶 ∈ 𝐵 → ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) )
11 5 10 orim12d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) → ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
12 11 con3d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ¬ ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) → ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
13 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
14 eloni ⊢ ( ( 𝐴 ·o 𝐵 ) ∈ On → Ord ( 𝐴 ·o 𝐵 ) )
15 13 14 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Ord ( 𝐴 ·o 𝐵 ) )
16 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ·o 𝐶 ) ∈ On )
17 eloni ⊢ ( ( 𝐴 ·o 𝐶 ) ∈ On → Ord ( 𝐴 ·o 𝐶 ) )
18 16 17 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → Ord ( 𝐴 ·o 𝐶 ) )
19 ordtri3 ⊢ ( ( Ord ( 𝐴 ·o 𝐵 ) ∧ Ord ( 𝐴 ·o 𝐶 ) ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) ↔ ¬ ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
20 15 18 19 syl2an ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) ↔ ¬ ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
21 20 3impdi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) ↔ ¬ ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
22 21 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) ↔ ¬ ( ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ∨ ( 𝐴 ·o 𝐶 ) ∈ ( 𝐴 ·o 𝐵 ) ) ) )
23 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
24 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
25 ordtri3 ⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
26 23 24 25 syl2an ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
27 26 3adant1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
28 27 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )
29 12 22 28 3imtr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) → 𝐵 = 𝐶 ) )
30 oveq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) )
31 29 30 impbid1 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o 𝐶 ) ↔ 𝐵 = 𝐶 ) )