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