Metamath Proof Explorer

Theorem 0hf

Description: The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015)

Ref Expression
Assertion 0hf 
|- (/) e. Hf

Proof

Step Hyp Ref Expression
1 peano1 
 |-  (/) e. _om
2 peano2 
 |-  ( (/) e. _om -> suc (/) e. _om )
3 1 2 ax-mp 
 |-  suc (/) e. _om
4 0elpw 
 |-  (/) e. ~P ( R1 ` (/) )
5 0elon 
 |-  (/) e. On
6 r1suc 
 |-  ( (/) e. On -> ( R1 ` suc (/) ) = ~P ( R1 ` (/) ) )
7 5 6 ax-mp 
 |-  ( R1 ` suc (/) ) = ~P ( R1 ` (/) )
8 4 7 eleqtrri 
 |-  (/) e. ( R1 ` suc (/) )
9 fveq2 
 |-  ( x = suc (/) -> ( R1 ` x ) = ( R1 ` suc (/) ) )
10 9 eleq2d 
 |-  ( x = suc (/) -> ( (/) e. ( R1 ` x ) <-> (/) e. ( R1 ` suc (/) ) ) )
11 10 rspcev 
 |-  ( ( suc (/) e. _om /\ (/) e. ( R1 ` suc (/) ) ) -> E. x e. _om (/) e. ( R1 ` x ) )
12 3 8 11 mp2an 
 |-  E. x e. _om (/) e. ( R1 ` x )
13 elhf 
 |-  ( (/) e. Hf <-> E. x e. _om (/) e. ( R1 ` x ) )
14 12 13 mpbir 
 |-  (/) e. Hf