Metamath Proof Explorer

Theorem omwordi

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

Ref Expression
Assertion omwordi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B

Proof

Step Hyp Ref Expression
1 omword ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ⊆ B ↔ C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
2 1 biimpd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ⊆ B → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
3 2 ex ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∅ ∈ C → A ⊆ B → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
4 eloni ⊢ C ∈ On → Ord ⁡ C
5 ord0eln0 ⊢ Ord ⁡ C → ∅ ∈ C ↔ C ≠ ∅
6 5 necon2bbid ⊢ Ord ⁡ C → C = ∅ ↔ ¬ ∅ ∈ C
7 4 6 syl ⊢ C ∈ On → C = ∅ ↔ ¬ ∅ ∈ C
8 7 3ad2ant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C = ∅ ↔ ¬ ∅ ∈ C
9 ssid ⊢ ∅ ⊆ ∅
10 om0r ⊢ A ∈ On → ∅ ⋅ 𝑜 A = ∅
11 10 adantr ⊢ A ∈ On ∧ B ∈ On → ∅ ⋅ 𝑜 A = ∅
12 om0r ⊢ B ∈ On → ∅ ⋅ 𝑜 B = ∅
13 12 adantl ⊢ A ∈ On ∧ B ∈ On → ∅ ⋅ 𝑜 B = ∅
14 11 13 sseq12d ⊢ A ∈ On ∧ B ∈ On → ∅ ⋅ 𝑜 A ⊆ ∅ ⋅ 𝑜 B ↔ ∅ ⊆ ∅
15 9 14 mpbiri ⊢ A ∈ On ∧ B ∈ On → ∅ ⋅ 𝑜 A ⊆ ∅ ⋅ 𝑜 B
16 oveq1 ⊢ C = ∅ → C ⋅ 𝑜 A = ∅ ⋅ 𝑜 A
17 oveq1 ⊢ C = ∅ → C ⋅ 𝑜 B = ∅ ⋅ 𝑜 B
18 16 17 sseq12d ⊢ C = ∅ → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B ↔ ∅ ⋅ 𝑜 A ⊆ ∅ ⋅ 𝑜 B
19 15 18 syl5ibrcom ⊢ A ∈ On ∧ B ∈ On → C = ∅ → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
20 19 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C = ∅ → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
21 8 20 sylbird ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ¬ ∅ ∈ C → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
22 21 a1dd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ¬ ∅ ∈ C → A ⊆ B → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B
23 3 22 pm2.61d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B → C ⋅ 𝑜 A ⊆ C ⋅ 𝑜 B