Theorem harn0

Description: The Hartogs number of a set is never zero.MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015)

	Ref	Expression
Assertion	harn0	$$⊢S\in V\to \mathrm{har}\left(S\right)\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0elon	$$⊢\varnothing \in \mathrm{On}$$
2	1	a1i	$$⊢S\in V\to \varnothing \in \mathrm{On}$$
3		0domg	$$⊢S\in V\to \varnothing \preccurlyeq S$$
4		elharval	$$⊢\varnothing \in \mathrm{har}\left(S\right)\leftrightarrow \left(\varnothing \in \mathrm{On}\wedge \varnothing \preccurlyeq S\right)$$
5	2 3 4	sylanbrc	$$⊢S\in V\to \varnothing \in \mathrm{har}\left(S\right)$$
6	5	ne0d	$$⊢S\in V\to \mathrm{har}\left(S\right)\ne \varnothing$$