Metamath Proof Explorer


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 } )