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	|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> B C_ ( A .o B ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	|- ( ( A e. On /\ B e. On ) <-> ( B e. On /\ A e. On ) )
2	1	anbi1i	|- ( ( ( A e. On /\ B e. On ) /\ A =/= (/) ) <-> ( ( B e. On /\ A e. On ) /\ A =/= (/) ) )
3		df-3an	|- ( ( A e. On /\ B e. On /\ A =/= (/) ) <-> ( ( A e. On /\ B e. On ) /\ A =/= (/) ) )
4		on0eln0	|- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
5	4	adantl	|- ( ( B e. On /\ A e. On ) -> ( (/) e. A <-> A =/= (/) ) )
6	5	pm5.32i	|- ( ( ( B e. On /\ A e. On ) /\ (/) e. A ) <-> ( ( B e. On /\ A e. On ) /\ A =/= (/) ) )
7	2 3 6	3bitr4i	|- ( ( A e. On /\ B e. On /\ A =/= (/) ) <-> ( ( B e. On /\ A e. On ) /\ (/) e. A ) )
8		omword2	|- ( ( ( B e. On /\ A e. On ) /\ (/) e. A ) -> B C_ ( A .o B ) )
9	7 8	sylbi	|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> B C_ ( A .o B ) )