Theorem infn0

Description: An infinite set is not empty. (Contributed by NM, 23-Oct-2004)

	Ref	Expression
Assertion	infn0	$$⊢\mathrm{\omega }\preccurlyeq A\to A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
2		infsdomnn	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge \varnothing \in \mathrm{\omega }\right)\to \varnothing \prec A$$
3	1 2	mpan2	$$⊢\mathrm{\omega }\preccurlyeq A\to \varnothing \prec A$$
4		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
5	4	brrelex2i	$$⊢\mathrm{\omega }\preccurlyeq A\to A\in \mathrm{V}$$
6		0sdomg	$$⊢A\in \mathrm{V}\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
7	5 6	syl	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
8	3 7	mpbid	$$⊢\mathrm{\omega }\preccurlyeq A\to A\ne \varnothing$$