Description: Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | harf | |- har : _V --> On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-har | |- har = ( x e. _V |-> { y e. On | y ~<_ x } ) |
|
2 | hartogs | |- ( x e. _V -> { y e. On | y ~<_ x } e. On ) |
|
3 | 1 2 | fmpti | |- har : _V --> On |