Metamath Proof Explorer

Theorem hfninf

Description: _om is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015)

Ref Expression
Assertion hfninf 
|- -. _om e. Hf

Proof

Step Hyp Ref Expression
1 elirr 
 |-  -. _om e. _om
2 elhf2g 
 |-  ( _om e. Hf -> ( _om e. Hf <-> ( rank ` _om ) e. _om ) )
3 ordom 
 |-  Ord _om
4 elong 
 |-  ( _om e. Hf -> ( _om e. On <-> Ord _om ) )
5 3 4 mpbiri 
 |-  ( _om e. Hf -> _om e. On )
6 r111 
 |-  R1 : On -1-1-> _V
7 f1dm 
 |-  ( R1 : On -1-1-> _V -> dom R1 = On )
8 6 7 ax-mp 
 |-  dom R1 = On
9 8 eleq2i 
 |-  ( _om e. dom R1 <-> _om e. On )
10 rankonid 
 |-  ( _om e. dom R1 <-> ( rank ` _om ) = _om )
11 9 10 bitr3i 
 |-  ( _om e. On <-> ( rank ` _om ) = _om )
12 5 11 sylib 
 |-  ( _om e. Hf -> ( rank ` _om ) = _om )
13 12 eleq1d 
 |-  ( _om e. Hf -> ( ( rank ` _om ) e. _om <-> _om e. _om ) )
14 2 13 bitrd 
 |-  ( _om e. Hf -> ( _om e. Hf <-> _om e. _om ) )
15 1 14 mtbiri 
 |-  ( _om e. Hf -> -. _om e. Hf )
16 pm2.01 
 |-  ( ( _om e. Hf -> -. _om e. Hf ) -> -. _om e. Hf )
17 15 16 ax-mp 
 |-  -. _om e. Hf