Theorem harf

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

	Ref	Expression
Assertion	harf	⊢ har : V ⟶ On

Proof

Step	Hyp	Ref	Expression
1		df-har	⊢ har = ( 𝑥 ∈ V ↦ { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑥 } )
2		hartogs	⊢ ( 𝑥 ∈ V → { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑥 } ∈ On )
3	1 2	fmpti	⊢ har : V ⟶ On