Theorem bnj158

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj158.1	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
Assertion	bnj158	$$⊢m\in D\to \exists p\in \mathrm{\omega }m=\mathrm{suc}p$$

Proof

Step	Hyp	Ref	Expression
1		bnj158.1	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
2	1	eleq2i	$$⊢m\in D\leftrightarrow m\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)$$
3		eldifsn	$$⊢m\in \left(\mathrm{\omega }\setminus \left\{\varnothing \right\}\right)\leftrightarrow \left(m\in \mathrm{\omega }\wedge m\ne \varnothing \right)$$
4	2 3	bitri	$$⊢m\in D\leftrightarrow \left(m\in \mathrm{\omega }\wedge m\ne \varnothing \right)$$
5		nnsuc	$$⊢\left(m\in \mathrm{\omega }\wedge m\ne \varnothing \right)\to \exists p\in \mathrm{\omega }m=\mathrm{suc}p$$
6	4 5	sylbi	$$⊢m\in D\to \exists p\in \mathrm{\omega }m=\mathrm{suc}p$$