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\in \left(\mathrm{On}\setminus 1_{𝑜}\right)\to \varnothing \in A$$

Proof

Step	Hyp	Ref	Expression
1		ondif1	$$⊢A\in \left(\mathrm{On}\setminus 1_{𝑜}\right)\leftrightarrow \left(A\in \mathrm{On}\wedge \varnothing \in A\right)$$
2	1	simprbi	$$⊢A\in \left(\mathrm{On}\setminus 1_{𝑜}\right)\to \varnothing \in A$$