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 ⊢A∈On∧B∈On∧C∈On∧∅∈A→A⋅𝑜B=A⋅𝑜C↔B=C

Proof

Step Hyp Ref Expression
1 omordi ⊢C∈On∧A∈On∧∅∈A→B∈C→A⋅𝑜B∈A⋅𝑜C
2 1 ex ⊢C∈On∧A∈On→∅∈A→B∈C→A⋅𝑜B∈A⋅𝑜C
3 2 ancoms ⊢A∈On∧C∈On→∅∈A→B∈C→A⋅𝑜B∈A⋅𝑜C
4 3 3adant2 ⊢A∈On∧B∈On∧C∈On→∅∈A→B∈C→A⋅𝑜B∈A⋅𝑜C
5 4 imp ⊢A∈On∧B∈On∧C∈On∧∅∈A→B∈C→A⋅𝑜B∈A⋅𝑜C
6 omordi ⊢B∈On∧A∈On∧∅∈A→C∈B→A⋅𝑜C∈A⋅𝑜B
7 6 ex ⊢B∈On∧A∈On→∅∈A→C∈B→A⋅𝑜C∈A⋅𝑜B
8 7 ancoms ⊢A∈On∧B∈On→∅∈A→C∈B→A⋅𝑜C∈A⋅𝑜B
9 8 3adant3 ⊢A∈On∧B∈On∧C∈On→∅∈A→C∈B→A⋅𝑜C∈A⋅𝑜B
10 9 imp ⊢A∈On∧B∈On∧C∈On∧∅∈A→C∈B→A⋅𝑜C∈A⋅𝑜B
11 5 10 orim12d ⊢A∈On∧B∈On∧C∈On∧∅∈A→B∈C∨C∈B→A⋅𝑜B∈A⋅𝑜C∨A⋅𝑜C∈A⋅𝑜B
12 11 con3d ⊢A∈On∧B∈On∧C∈On∧∅∈A→¬A⋅𝑜B∈A⋅𝑜C∨A⋅𝑜C∈A⋅𝑜B→¬B∈C∨C∈B
13 omcl ⊢A∈On∧B∈On→A⋅𝑜B∈On
14 eloni ⊢A⋅𝑜B∈On→Ord⁡A⋅𝑜B
15 13 14 syl ⊢A∈On∧B∈On→Ord⁡A⋅𝑜B
16 omcl ⊢A∈On∧C∈On→A⋅𝑜C∈On
17 eloni ⊢A⋅𝑜C∈On→Ord⁡A⋅𝑜C
18 16 17 syl ⊢A∈On∧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 15 18 19 syl2an ⊢A∈On∧B∈On∧A∈On∧C∈On→A⋅𝑜B=A⋅𝑜C↔¬A⋅𝑜B∈A⋅𝑜C∨A⋅𝑜C∈A⋅𝑜B
21 20 3impdi ⊢A∈On∧B∈On∧C∈On→A⋅𝑜B=A⋅𝑜C↔¬A⋅𝑜B∈A⋅𝑜C∨A⋅𝑜C∈A⋅𝑜B
22 21 adantr ⊢A∈On∧B∈On∧C∈On∧∅∈A→A⋅𝑜B=A⋅𝑜C↔¬A⋅𝑜B∈A⋅𝑜C∨A⋅𝑜C∈A⋅𝑜B
23 eloni ⊢B∈On→Ord⁡B
24 eloni ⊢C∈On→Ord⁡C
25 ordtri3 ⊢Ord⁡B∧Ord⁡C→B=C↔¬B∈C∨C∈B
26 23 24 25 syl2an ⊢B∈On∧C∈On→B=C↔¬B∈C∨C∈B
27 26 3adant1 ⊢A∈On∧B∈On∧C∈On→B=C↔¬B∈C∨C∈B
28 27 adantr ⊢A∈On∧B∈On∧C∈On∧∅∈A→B=C↔¬B∈C∨C∈B
29 12 22 28 3imtr4d ⊢A∈On∧B∈On∧C∈On∧∅∈A→A⋅𝑜B=A⋅𝑜C→B=C
30 oveq2 ⊢B=C→A⋅𝑜B=A⋅𝑜C
31 29 30 impbid1 ⊢A∈On∧B∈On∧C∈On∧∅∈A→A⋅𝑜B=A⋅𝑜C↔B=C