Theorem ordgt0ge1

Description: Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004)

	Ref	Expression
Assertion	ordgt0ge1	$$⊢\mathrm{Ord}A\to \left(\varnothing \in A\leftrightarrow 1_{𝑜}\subseteq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		0elon	$$⊢\varnothing \in \mathrm{On}$$
2		ordelsuc	$$⊢\left(\varnothing \in \mathrm{On}\wedge \mathrm{Ord}A\right)\to \left(\varnothing \in A\leftrightarrow \mathrm{suc}\varnothing \subseteq A\right)$$
3	1 2	mpan	$$⊢\mathrm{Ord}A\to \left(\varnothing \in A\leftrightarrow \mathrm{suc}\varnothing \subseteq A\right)$$
4		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
5	4	sseq1i	$$⊢1_{𝑜}\subseteq A\leftrightarrow \mathrm{suc}\varnothing \subseteq A$$
6	3 5	bitr4di	$$⊢\mathrm{Ord}A\to \left(\varnothing \in A\leftrightarrow 1_{𝑜}\subseteq A\right)$$