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 |
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 |