Metamath Proof Explorer

Theorem nnmword

Description: Weak ordering property of ordinal multiplication. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion nnmword ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → A ⊆ B ↔ C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B

Proof

Step Hyp Ref Expression
1 iba ⊢ ∅ ∈ C → B ∈ A ↔ B ∈ A ∧ ∅ ∈ C
2 nnmord ⊢ B ∈ ω ∧ A ∈ ω ∧ C ∈ ω → B ∈ A ∧ ∅ ∈ C ↔ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
3 2 3com12 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → B ∈ A ∧ ∅ ∈ C ↔ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
4 1 3 sylan9bbr ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → B ∈ A ↔ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
5 4 notbid ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → ¬ B ∈ A ↔ ¬ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
6 simpl1 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → A ∈ ω
7 nnon ⊢ A ∈ ω → A ∈ On
8 6 7 syl ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → A ∈ On
9 simpl2 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → B ∈ ω
10 nnon ⊢ B ∈ ω → B ∈ On
11 9 10 syl ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → B ∈ On
12 ontri1 ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ¬ B ∈ A
13 8 11 12 syl2anc ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → A ⊆ B ↔ ¬ B ∈ A
14 simpl3 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → C ∈ ω
15 nnmcl ⊢ C ∈ ω ∧ A ∈ ω → C ⋅ 𝑜 A ∈ ω
16 14 6 15 syl2anc ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → C ⋅ 𝑜 A ∈ ω
17 nnon ⊢ C ⋅ 𝑜 A ∈ ω → C ⋅ 𝑜 A ∈ On
18 16 17 syl ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → C ⋅ 𝑜 A ∈ On
19 nnmcl ⊢ C ∈ ω ∧ B ∈ ω → C ⋅ 𝑜 B ∈ ω
20 14 9 19 syl2anc ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → C ⋅ 𝑜 B ∈ ω
21 nnon ⊢ C ⋅ 𝑜 B ∈ ω → C ⋅ 𝑜 B ∈ On
22 20 21 syl ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → C ⋅ 𝑜 B ∈ On
23 ontri1 ⊢ C ⋅ 𝑜 A ∈ On ∧ C ⋅ 𝑜 B ∈ On → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B ↔ ¬ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
24 18 22 23 syl2anc ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B ↔ ¬ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
25 5 13 24 3bitr4d ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → A ⊆ B ↔ C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B