Metamath Proof Explorer


Theorem omword2

Description: An ordinal is less than or equal to its product with another. (Contributed by NM, 21-Dec-2004)

Ref Expression
Assertion omword2 ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → 𝐴 ⊆ ( 𝐵 ·o 𝐴 ) )

Proof

Step Hyp Ref Expression
1 om1r ( 𝐴 ∈ On → ( 1o ·o 𝐴 ) = 𝐴 )
2 1 ad2antrr ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → ( 1o ·o 𝐴 ) = 𝐴 )
3 eloni ( 𝐵 ∈ On → Ord 𝐵 )
4 ordgt0ge1 ( Ord 𝐵 → ( ∅ ∈ 𝐵 ↔ 1o𝐵 ) )
5 4 biimpa ( ( Ord 𝐵 ∧ ∅ ∈ 𝐵 ) → 1o𝐵 )
6 3 5 sylan ( ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) → 1o𝐵 )
7 6 adantll ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → 1o𝐵 )
8 1on 1o ∈ On
9 omwordri ( ( 1o ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 1o𝐵 → ( 1o ·o 𝐴 ) ⊆ ( 𝐵 ·o 𝐴 ) ) )
10 8 9 mp3an1 ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 1o𝐵 → ( 1o ·o 𝐴 ) ⊆ ( 𝐵 ·o 𝐴 ) ) )
11 10 ancoms ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 1o𝐵 → ( 1o ·o 𝐴 ) ⊆ ( 𝐵 ·o 𝐴 ) ) )
12 11 adantr ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → ( 1o𝐵 → ( 1o ·o 𝐴 ) ⊆ ( 𝐵 ·o 𝐴 ) ) )
13 7 12 mpd ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → ( 1o ·o 𝐴 ) ⊆ ( 𝐵 ·o 𝐴 ) )
14 2 13 eqsstrrd ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → 𝐴 ⊆ ( 𝐵 ·o 𝐴 ) )