Metamath Proof Explorer


Theorem ominf4

Description: _om is Dedekind infinite. (Contributed by Stefan O'Rear, 30-Oct-2014) (Proof shortened by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion ominf4
|- -. _om e. Fin4

Proof

Step Hyp Ref Expression
1 id
 |-  ( _om e. Fin4 -> _om e. Fin4 )
2 peano1
 |-  (/) e. _om
3 difsnpss
 |-  ( (/) e. _om <-> ( _om \ { (/) } ) C. _om )
4 2 3 mpbi
 |-  ( _om \ { (/) } ) C. _om
5 limom
 |-  Lim _om
6 5 limenpsi
 |-  ( _om e. Fin4 -> _om ~~ ( _om \ { (/) } ) )
7 6 ensymd
 |-  ( _om e. Fin4 -> ( _om \ { (/) } ) ~~ _om )
8 fin4i
 |-  ( ( ( _om \ { (/) } ) C. _om /\ ( _om \ { (/) } ) ~~ _om ) -> -. _om e. Fin4 )
9 4 7 8 sylancr
 |-  ( _om e. Fin4 -> -. _om e. Fin4 )
10 1 9 pm2.65i
 |-  -. _om e. Fin4