Theorem ondif1

Description: Two ways to say that A is a nonzero ordinal number. Lemma 1.10 of Schloeder p. 2. (Contributed by Mario Carneiro, 21-May-2015)

	Ref	Expression
Assertion	ondif1	$$⊢A\in \left(\mathrm{On}\setminus 1_{𝑜}\right)\leftrightarrow \left(A\in \mathrm{On}\wedge \varnothing \in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dif1o	$$⊢A\in \left(\mathrm{On}\setminus 1_{𝑜}\right)\leftrightarrow \left(A\in \mathrm{On}\wedge A\ne \varnothing \right)$$
2		on0eln0	$$⊢A\in \mathrm{On}\to \left(\varnothing \in A\leftrightarrow A\ne \varnothing \right)$$
3	2	pm5.32i	$$⊢\left(A\in \mathrm{On}\wedge \varnothing \in A\right)\leftrightarrow \left(A\in \mathrm{On}\wedge A\ne \varnothing \right)$$
4	1 3	bitr4i	$$⊢A\in \left(\mathrm{On}\setminus 1_{𝑜}\right)\leftrightarrow \left(A\in \mathrm{On}\wedge \varnothing \in A\right)$$