Metamath Proof Explorer


Theorem harf

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

Ref Expression
Assertion harf
|- har : _V --> On

Proof

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