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 V har S

Proof

Step Hyp Ref Expression
1 0elon On
2 1 a1i S V On
3 0domg S V S
4 elharval har S On S
5 2 3 4 sylanbrc S V har S
6 5 ne0d S V har S