Theorem harval

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

	Ref	Expression
Assertion	harval	|- ( X e. V -> ( har ` X ) = { y e. On | y ~<_ X } )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( X e. V -> X e. _V )
2		breq2	|- ( x = X -> ( y ~<_ x <-> y ~<_ X ) )
3	2	rabbidv	|- ( x = X -> { y e. On | y ~<_ x } = { y e. On | y ~<_ X } )
4		df-har	|- har = ( x e. _V |-> { y e. On | y ~<_ x } )
5		hartogs	|- ( x e. _V -> { y e. On | y ~<_ x } e. On )
6	3 4 5	fvmpt3	|- ( X e. _V -> ( har ` X ) = { y e. On | y ~<_ X } )
7	1 6	syl	|- ( X e. V -> ( har ` X ) = { y e. On | y ~<_ X } )