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