Theorem ordge1n0

Description: An ordinal greater than or equal to 1 is nonzero. (Contributed by NM, 21-Dec-2004)

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

Proof

Step	Hyp	Ref	Expression
1		ordgt0ge1	$$⊢\mathrm{Ord}A\to \left(\varnothing \in A\leftrightarrow 1_{𝑜}\subseteq A\right)$$
2		ord0eln0	$$⊢\mathrm{Ord}A\to \left(\varnothing \in A\leftrightarrow A\ne \varnothing \right)$$
3	1 2	bitr3d	$$⊢\mathrm{Ord}A\to \left(1_{𝑜}\subseteq A\leftrightarrow A\ne \varnothing \right)$$