This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
2 ordgt0ge1 ⊢ ( Ord 𝐵 → ( ∅ ∈ 𝐵 ↔ 1o ⊆ 𝐵 ) )
3 1 2 syl ⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ 1o ⊆ 𝐵 ) )
4 3 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐵 ↔ 1o ⊆ 𝐵 ) )
5 1on ⊢ 1o ∈ On
6 omwordi ⊢ ( ( 1o ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 1o ⊆ 𝐵 → ( 𝐴 ·o 1o ) ⊆ ( 𝐴 ·o 𝐵 ) ) )
7 5 6 mp3an1 ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 1o ⊆ 𝐵 → ( 𝐴 ·o 1o ) ⊆ ( 𝐴 ·o 𝐵 ) ) )
8 7 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 1o ⊆ 𝐵 → ( 𝐴 ·o 1o ) ⊆ ( 𝐴 ·o 𝐵 ) ) )
9 om1 ⊢ ( 𝐴 ∈ On → ( 𝐴 ·o 1o ) = 𝐴 )
10 9 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 1o ) = 𝐴 )
11 10 sseq1d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 1o ) ⊆ ( 𝐴 ·o 𝐵 ) ↔ 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) ) )
12 8 11 sylibd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 1o ⊆ 𝐵 → 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) ) )
13 4 12 sylbid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐵 → 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) ) )
14 13 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) )