Metamath Proof Explorer

Theorem omword1

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

Ref Expression
Assertion omword1 ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ B → A ⊆ A ⋅ 𝑜 B

Proof

Step Hyp Ref Expression
1 eloni ⊢ B ∈ On → Ord ⁡ B
2 ordgt0ge1 ⊢ Ord ⁡ B → ∅ ∈ B ↔ 1 𝑜 ⊆ B
3 1 2 syl ⊢ B ∈ On → ∅ ∈ B ↔ 1 𝑜 ⊆ B
4 3 adantl ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ B ↔ 1 𝑜 ⊆ B
5 1on ⊢ 1 𝑜 ∈ On
6 omwordi ⊢ 1 𝑜 ∈ On ∧ B ∈ On ∧ A ∈ On → 1 𝑜 ⊆ B → A ⋅ 𝑜 1 𝑜 ⊆ A ⋅ 𝑜 B
7 5 6 mp3an1 ⊢ B ∈ On ∧ A ∈ On → 1 𝑜 ⊆ B → A ⋅ 𝑜 1 𝑜 ⊆ A ⋅ 𝑜 B
8 7 ancoms ⊢ A ∈ On ∧ B ∈ On → 1 𝑜 ⊆ B → A ⋅ 𝑜 1 𝑜 ⊆ A ⋅ 𝑜 B
9 om1 ⊢ A ∈ On → A ⋅ 𝑜 1 𝑜 = A
10 9 adantr ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 1 𝑜 = A
11 10 sseq1d ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 1 𝑜 ⊆ A ⋅ 𝑜 B ↔ A ⊆ A ⋅ 𝑜 B
12 8 11 sylibd ⊢ A ∈ On ∧ B ∈ On → 1 𝑜 ⊆ B → A ⊆ A ⋅ 𝑜 B
13 4 12 sylbid ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ B → A ⊆ A ⋅ 𝑜 B
14 13 imp ⊢ A ∈ On ∧ B ∈ On ∧ ∅ ∈ B → A ⊆ A ⋅ 𝑜 B