Metamath Proof Explorer

Theorem omword1

Description: An ordinal is less than or equal to its product with another. Lemma 3.11 of Schloeder p. 8. (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