Theorem elharval

Description: The Hartogs number of a set contains exactly the ordinals that set dominates. Combined with harcl , this implies that the Hartogs number of a set is greater than all ordinals that set dominates. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	elharval	$$⊢Y\in \mathrm{har}\left(X\right)\leftrightarrow \left(Y\in \mathrm{On}\wedge Y\preccurlyeq X\right)$$

Proof

Step	Hyp	Ref	Expression
1		elfvex	$$⊢Y\in \mathrm{har}\left(X\right)\to X\in \mathrm{V}$$
2		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
3	2	brrelex2i	$$⊢Y\preccurlyeq X\to X\in \mathrm{V}$$
4	3	adantl	$$⊢\left(Y\in \mathrm{On}\wedge Y\preccurlyeq X\right)\to X\in \mathrm{V}$$
5		harval	$$⊢X\in \mathrm{V}\to \mathrm{har}\left(X\right)=\left\{y\in \mathrm{On}|y\preccurlyeq X\right\}$$
6	5	eleq2d	$$⊢X\in \mathrm{V}\to \left(Y\in \mathrm{har}\left(X\right)\leftrightarrow Y\in \left\{y\in \mathrm{On}|y\preccurlyeq X\right\}\right)$$
7		breq1	$$⊢y=Y\to \left(y\preccurlyeq X\leftrightarrow Y\preccurlyeq X\right)$$
8	7	elrab	$$⊢Y\in \left\{y\in \mathrm{On}|y\preccurlyeq X\right\}\leftrightarrow \left(Y\in \mathrm{On}\wedge Y\preccurlyeq X\right)$$
9	6 8	bitrdi	$$⊢X\in \mathrm{V}\to \left(Y\in \mathrm{har}\left(X\right)\leftrightarrow \left(Y\in \mathrm{On}\wedge Y\preccurlyeq X\right)\right)$$
10	1 4 9	pm5.21nii	$$⊢Y\in \mathrm{har}\left(X\right)\leftrightarrow \left(Y\in \mathrm{On}\wedge Y\preccurlyeq X\right)$$