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 ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ B → A ⊆ B ⋅ 𝑜 A

Proof

Step Hyp Ref Expression
1 om1r ⊢ A ∈ On → 1 𝑜 ⋅ 𝑜 A = A
2 1 ad2antrr ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ B → 1 𝑜 ⋅ 𝑜 A = A
3 eloni ⊢ B ∈ On → Ord ⁡ B
4 ordgt0ge1 ⊢ Ord ⁡ B → ∅ ∈ B ↔ 1 𝑜 ⊆ B
5 4 biimpa ⊢ Ord ⁡ B ∧ ∅ ∈ B → 1 𝑜 ⊆ B
6 3 5 sylan ⊢ B ∈ On ∧ ∅ ∈ B → 1 𝑜 ⊆ B
7 6 adantll ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ B → 1 𝑜 ⊆ B
8 1on ⊢ 1 𝑜 ∈ On
9 omwordri ⊢ 1 𝑜 ∈ On ∧ B ∈ On ∧ A ∈ On → 1 𝑜 ⊆ B → 1 𝑜 ⋅ 𝑜 A ⊆ B ⋅ 𝑜 A
10 8 9 mp3an1 ⊢ B ∈ On ∧ A ∈ On → 1 𝑜 ⊆ B → 1 𝑜 ⋅ 𝑜 A ⊆ B ⋅ 𝑜 A
11 10 ancoms ⊢ A ∈ On ∧ B ∈ On → 1 𝑜 ⊆ B → 1 𝑜 ⋅ 𝑜 A ⊆ B ⋅ 𝑜 A
12 11 adantr ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ B → 1 𝑜 ⊆ B → 1 𝑜 ⋅ 𝑜 A ⊆ B ⋅ 𝑜 A
13 7 12 mpd ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ B → 1 𝑜 ⋅ 𝑜 A ⊆ B ⋅ 𝑜 A
14 2 13 eqsstrrd ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ B → A ⊆ B ⋅ 𝑜 A