Theorem ondif1i

Description: Ordinal zero is less than every non-zero ordinal, class difference version. Theorem 1.10 of Schloeder p. 2. See ondif1 . (Contributed by RP, 16-Jan-2025)

	Ref	Expression
Assertion	ondif1i	|- ( A e. ( On \ 1o ) -> (/) e. A )

Proof

Step	Hyp	Ref	Expression
1		ondif1	|- ( A e. ( On \ 1o ) <-> ( A e. On /\ (/) e. A ) )
2	1	simprbi	|- ( A e. ( On \ 1o ) -> (/) e. A )