Theorem nsuceq0

Description: No successor is empty. (Contributed by NM, 3-Apr-1995)

	Ref	Expression
Assertion	nsuceq0	$$⊢\mathrm{suc}A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg A\in \varnothing$$
2		sucidg	$$⊢A\in \mathrm{V}\to A\in \mathrm{suc}A$$
3		eleq2	$$⊢\mathrm{suc}A=\varnothing \to \left(A\in \mathrm{suc}A\leftrightarrow A\in \varnothing \right)$$
4	2 3	syl5ibcom	$$⊢A\in \mathrm{V}\to \left(\mathrm{suc}A=\varnothing \to A\in \varnothing \right)$$
5	1 4	mtoi	$$⊢A\in \mathrm{V}\to \neg \mathrm{suc}A=\varnothing$$
6		0ex	$$⊢\varnothing \in \mathrm{V}$$
7		eleq1	$$⊢A=\varnothing \to \left(A\in \mathrm{V}\leftrightarrow \varnothing \in \mathrm{V}\right)$$
8	6 7	mpbiri	$$⊢A=\varnothing \to A\in \mathrm{V}$$
9	8	con3i	$$⊢\neg A\in \mathrm{V}\to \neg A=\varnothing$$
10		sucprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{suc}A=A$$
11	10	eqeq1d	$$⊢\neg A\in \mathrm{V}\to \left(\mathrm{suc}A=\varnothing \leftrightarrow A=\varnothing \right)$$
12	9 11	mtbird	$$⊢\neg A\in \mathrm{V}\to \neg \mathrm{suc}A=\varnothing$$
13	5 12	pm2.61i	$$⊢\neg \mathrm{suc}A=\varnothing$$
14	13	neir	$$⊢\mathrm{suc}A\ne \varnothing$$