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