Theorem omge2

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

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

Proof

Step	Hyp	Ref	Expression
1		ancom	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ↔ ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) )
2	1	anbi1i	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ≠ ∅ ) ↔ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) ∧ 𝐴 ≠ ∅ ) )
3		df-3an	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ↔ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ≠ ∅ ) )
4		on0eln0	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
5	4	adantl	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
6	5	pm5.32i	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) ↔ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) ∧ 𝐴 ≠ ∅ ) )
7	2 3 6	3bitr4i	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ↔ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) )
8		omword2	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → 𝐵 ⊆ ( 𝐴 ·o 𝐵 ) )
9	7 8	sylbi	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → 𝐵 ⊆ ( 𝐴 ·o 𝐵 ) )