Theorem omword2

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

	Ref	Expression
Assertion	omword2	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → 𝐴 ⊆ ( 𝐵 ·o 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		om1r	⊢ ( 𝐴 ∈ On → ( 1o ·o 𝐴 ) = 𝐴 )
2	1	ad2antrr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → ( 1o ·o 𝐴 ) = 𝐴 )
3		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
4		ordgt0ge1	⊢ ( Ord 𝐵 → ( ∅ ∈ 𝐵 ↔ 1o ⊆ 𝐵 ) )
5	4	biimpa	⊢ ( ( Ord 𝐵 ∧ ∅ ∈ 𝐵 ) → 1o ⊆ 𝐵 )
6	3 5	sylan	⊢ ( ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) → 1o ⊆ 𝐵 )
7	6	adantll	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → 1o ⊆ 𝐵 )
8		1on	⊢ 1o ∈ On
9		omwordri	⊢ ( ( 1o ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 1o ⊆ 𝐵 → ( 1o ·o 𝐴 ) ⊆ ( 𝐵 ·o 𝐴 ) ) )
10	8 9	mp3an1	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 1o ⊆ 𝐵 → ( 1o ·o 𝐴 ) ⊆ ( 𝐵 ·o 𝐴 ) ) )
11	10	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 1o ⊆ 𝐵 → ( 1o ·o 𝐴 ) ⊆ ( 𝐵 ·o 𝐴 ) ) )
12	11	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → ( 1o ⊆ 𝐵 → ( 1o ·o 𝐴 ) ⊆ ( 𝐵 ·o 𝐴 ) ) )
13	7 12	mpd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → ( 1o ·o 𝐴 ) ⊆ ( 𝐵 ·o 𝐴 ) )
14	2 13	eqsstrrd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → 𝐴 ⊆ ( 𝐵 ·o 𝐴 ) )