Metamath Proof Explorer

Theorem harn0

Description: The Hartogs number of a set is never zero.MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015)

Ref Expression
Assertion harn0 
|- ( S e. V -> ( har ` S ) =/= (/) )

Proof

Step Hyp Ref Expression
1 0elon 
 |-  (/) e. On
2 1 a1i 
 |-  ( S e. V -> (/) e. On )
3 0domg 
 |-  ( S e. V -> (/) ~<_ S )
4 elharval 
 |-  ( (/) e. ( har ` S ) <-> ( (/) e. On /\ (/) ~<_ S ) )
5 2 3 4 sylanbrc 
 |-  ( S e. V -> (/) e. ( har ` S ) )
6 5 ne0d 
 |-  ( S e. V -> ( har ` S ) =/= (/) )