Metamath Proof Explorer

Theorem nnmwordi

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

Ref Expression
Assertion nnmwordi ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nnmword ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) )
2 1 biimpd ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) )
3 2 ex ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ∅ ∈ 𝐶 → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) ) )
4 nnord ⊢ ( 𝐶 ∈ ω → Ord 𝐶 )
5 ord0eln0 ⊢ ( Ord 𝐶 → ( ∅ ∈ 𝐶 ↔ 𝐶 ≠ ∅ ) )
6 5 necon2bbid ⊢ ( Ord 𝐶 → ( 𝐶 = ∅ ↔ ¬ ∅ ∈ 𝐶 ) )
7 4 6 syl ⊢ ( 𝐶 ∈ ω → ( 𝐶 = ∅ ↔ ¬ ∅ ∈ 𝐶 ) )
8 7 3ad2ant3 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐶 = ∅ ↔ ¬ ∅ ∈ 𝐶 ) )
9 ssid ⊢ ∅ ⊆ ∅
10 nnm0r ⊢ ( 𝐴 ∈ ω → ( ∅ ·o 𝐴 ) = ∅ )
11 10 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ∅ ·o 𝐴 ) = ∅ )
12 nnm0r ⊢ ( 𝐵 ∈ ω → ( ∅ ·o 𝐵 ) = ∅ )
13 12 adantl ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ∅ ·o 𝐵 ) = ∅ )
14 11 13 sseq12d ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( ∅ ·o 𝐴 ) ⊆ ( ∅ ·o 𝐵 ) ↔ ∅ ⊆ ∅ ) )
15 9 14 mpbiri ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ∅ ·o 𝐴 ) ⊆ ( ∅ ·o 𝐵 ) )
16 oveq1 ⊢ ( 𝐶 = ∅ → ( 𝐶 ·o 𝐴 ) = ( ∅ ·o 𝐴 ) )
17 oveq1 ⊢ ( 𝐶 = ∅ → ( 𝐶 ·o 𝐵 ) = ( ∅ ·o 𝐵 ) )
18 16 17 sseq12d ⊢ ( 𝐶 = ∅ → ( ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ↔ ( ∅ ·o 𝐴 ) ⊆ ( ∅ ·o 𝐵 ) ) )
19 15 18 syl5ibrcom ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐶 = ∅ → ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) )
20 19 3adant3 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐶 = ∅ → ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) )
21 8 20 sylbird ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ¬ ∅ ∈ 𝐶 → ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) )
22 21 a1dd ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ¬ ∅ ∈ 𝐶 → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) ) )
23 3 22 pm2.61d ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) )