Theorem harval

Description: Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Assertion	harval	$$⊢X\in V\to \mathrm{har}\left(X\right)=\left\{y\in \mathrm{On}|y\preccurlyeq X\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢X\in V\to X\in \mathrm{V}$$
2		breq2	$$⊢x=X\to \left(y\preccurlyeq x\leftrightarrow y\preccurlyeq X\right)$$
3	2	rabbidv	$$⊢x=X\to \left\{y\in \mathrm{On}|y\preccurlyeq x\right\}=\left\{y\in \mathrm{On}|y\preccurlyeq X\right\}$$
4		df-har	$$⊢\mathrm{har}=\left(x\in \mathrm{V}⟼\left\{y\in \mathrm{On}|y\preccurlyeq x\right\}\right)$$
5		hartogs	$$⊢x\in \mathrm{V}\to \left\{y\in \mathrm{On}|y\preccurlyeq x\right\}\in \mathrm{On}$$
6	3 4 5	fvmpt3	$$⊢X\in \mathrm{V}\to \mathrm{har}\left(X\right)=\left\{y\in \mathrm{On}|y\preccurlyeq X\right\}$$
7	1 6	syl	$$⊢X\in V\to \mathrm{har}\left(X\right)=\left\{y\in \mathrm{On}|y\preccurlyeq X\right\}$$