Metamath Proof Explorer

Theorem omwordi

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

Ref Expression
Assertion omwordi ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ·o 𝐴 ) ⊆ ( 𝐶 ·o 𝐵 ) ) )

Proof

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