Theorem omge1

Description: Any non-zero ordinal product is greater-than-or-equal to the term on the left. Lemma 3.11 of Schloeder p. 8. See omword1 . (Contributed by RP, 29-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		3simpa	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) )
2		on0eln0	⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅ ) )
3	2	biimpar	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → ∅ ∈ 𝐵 )
4	3	3adant1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → ∅ ∈ 𝐵 )
5		omword1	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) )
6	1 4 5	syl2anc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) )