Theorem 0elsuc

Description: The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995)

	Ref	Expression
Assertion	0elsuc	$$⊢\mathrm{Ord}A\to \varnothing \in \mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		ordsuc	$$⊢\mathrm{Ord}A\leftrightarrow \mathrm{Ord}\mathrm{suc}A$$
2		nsuceq0	$$⊢\mathrm{suc}A\ne \varnothing$$
3		ord0eln0	$$⊢\mathrm{Ord}\mathrm{suc}A\to \left(\varnothing \in \mathrm{suc}A\leftrightarrow \mathrm{suc}A\ne \varnothing \right)$$
4	2 3	mpbiri	$$⊢\mathrm{Ord}\mathrm{suc}A\to \varnothing \in \mathrm{suc}A$$
5	1 4	sylbi	$$⊢\mathrm{Ord}A\to \varnothing \in \mathrm{suc}A$$