Metamath Proof Explorer

Theorem omword

Description: Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004)

Ref Expression
Assertion omword ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ⊆ B ↔ C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B

Proof

Step Hyp Ref Expression
1 omord2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ B ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
2 3anrot ⊢ C ∈ On ∧ A ∈ On ∧ B ∈ On ↔ A ∈ On ∧ B ∈ On ∧ C ∈ On
3 omcan ⊢ C ∈ On ∧ A ∈ On ∧ B ∈ On ∧ ∅ ∈ C → C ⋅ 𝑜 A = C ⋅ 𝑜 B ↔ A = B
4 2 3 sylanbr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → C ⋅ 𝑜 A = C ⋅ 𝑜 B ↔ A = B
5 4 bicomd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A = B ↔ C ⋅ 𝑜 A = C ⋅ 𝑜 B
6 1 5 orbi12d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ B ∨ A = B ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ∨ C ⋅ 𝑜 A = C ⋅ 𝑜 B
7 onsseleq ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ A ∈ B ∨ A = B
8 7 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B ↔ A ∈ B ∨ A = B
9 8 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ⊆ B ↔ A ∈ B ∨ A = B
10 omcl ⊢ C ∈ On ∧ A ∈ On → C ⋅ 𝑜 A ∈ On
11 omcl ⊢ C ∈ On ∧ B ∈ On → C ⋅ 𝑜 B ∈ On
12 10 11 anim12dan ⊢ C ∈ On ∧ A ∈ On ∧ B ∈ On → C ⋅ 𝑜 A ∈ On ∧ C ⋅ 𝑜 B ∈ On
13 12 ancoms ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ⋅ 𝑜 A ∈ On ∧ C ⋅ 𝑜 B ∈ On
14 13 3impa ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ⋅ 𝑜 A ∈ On ∧ C ⋅ 𝑜 B ∈ On
15 onsseleq ⊢ C ⋅ 𝑜 A ∈ On ∧ C ⋅ 𝑜 B ∈ On → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ∨ C ⋅ 𝑜 A = C ⋅ 𝑜 B
16 14 15 syl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ∨ C ⋅ 𝑜 A = C ⋅ 𝑜 B
17 16 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ∨ C ⋅ 𝑜 A = C ⋅ 𝑜 B
18 6 9 17 3bitr4d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ⊆ B ↔ C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B