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 𝐵 ) )