Theorem harf

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

	Ref	Expression
Assertion	harf	$$⊢\mathrm{har}:\mathrm{V}⟶\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		df-har	$$⊢\mathrm{har}=\left(x\in \mathrm{V}⟼\left\{y\in \mathrm{On}|y\preccurlyeq x\right\}\right)$$
2		hartogs	$$⊢x\in \mathrm{V}\to \left\{y\in \mathrm{On}|y\preccurlyeq x\right\}\in \mathrm{On}$$
3	1 2	fmpti	$$⊢\mathrm{har}:\mathrm{V}⟶\mathrm{On}$$