Theorem harval

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

	Ref	Expression
Assertion	harval	⊢ ( 𝑋 ∈ 𝑉 → ( har ‘ 𝑋 ) = { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑋 } )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ V )
2		breq2	⊢ ( 𝑥 = 𝑋 → ( 𝑦 ≼ 𝑥 ↔ 𝑦 ≼ 𝑋 ) )
3	2	rabbidv	⊢ ( 𝑥 = 𝑋 → { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑥 } = { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑋 } )
4		df-har	⊢ har = ( 𝑥 ∈ V ↦ { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑥 } )
5		hartogs	⊢ ( 𝑥 ∈ V → { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑥 } ∈ On )
6	3 4 5	fvmpt3	⊢ ( 𝑋 ∈ V → ( har ‘ 𝑋 ) = { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑋 } )
7	1 6	syl	⊢ ( 𝑋 ∈ 𝑉 → ( har ‘ 𝑋 ) = { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑋 } )