This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infn0

Description: An infinite set is not empty. For a shorter proof using ax-un , see infn0ALT . (Contributed by NM, 23-Oct-2004) Avoid ax-un . (Revised by BTernaryTau, 8-Jan-2025)

Ref Expression
Assertion infn0 
|- ( _om ~<_ A -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 brdomi 
 |-  ( _om ~<_ A -> E. f f : _om -1-1-> A )
2 peano1 
 |-  (/) e. _om
3 f1f1orn 
 |-  ( f : _om -1-1-> A -> f : _om -1-1-onto-> ran f )
4 3 adantr 
 |-  ( ( f : _om -1-1-> A /\ A = (/) ) -> f : _om -1-1-onto-> ran f )
5 f1f 
 |-  ( f : _om -1-1-> A -> f : _om --> A )
6 5 frnd 
 |-  ( f : _om -1-1-> A -> ran f C_ A )
7 sseq0 
 |-  ( ( ran f C_ A /\ A = (/) ) -> ran f = (/) )
8 6 7 sylan 
 |-  ( ( f : _om -1-1-> A /\ A = (/) ) -> ran f = (/) )
9 8 f1oeq3d 
 |-  ( ( f : _om -1-1-> A /\ A = (/) ) -> ( f : _om -1-1-onto-> ran f <-> f : _om -1-1-onto-> (/) ) )
10 4 9 mpbid 
 |-  ( ( f : _om -1-1-> A /\ A = (/) ) -> f : _om -1-1-onto-> (/) )
11 f1ocnv 
 |-  ( f : _om -1-1-onto-> (/) -> `' f : (/) -1-1-onto-> _om )
12 noel 
 |-  -. (/) e. (/)
13 f1o00 
 |-  ( `' f : (/) -1-1-onto-> _om <-> ( `' f = (/) /\ _om = (/) ) )
14 13 simprbi 
 |-  ( `' f : (/) -1-1-onto-> _om -> _om = (/) )
15 14 eleq2d 
 |-  ( `' f : (/) -1-1-onto-> _om -> ( (/) e. _om <-> (/) e. (/) ) )
16 12 15 mtbiri 
 |-  ( `' f : (/) -1-1-onto-> _om -> -. (/) e. _om )
17 10 11 16 3syl 
 |-  ( ( f : _om -1-1-> A /\ A = (/) ) -> -. (/) e. _om )
18 2 17 mt2 
 |-  -. ( f : _om -1-1-> A /\ A = (/) )
19 18 imnani 
 |-  ( f : _om -1-1-> A -> -. A = (/) )
20 19 neqned 
 |-  ( f : _om -1-1-> A -> A =/= (/) )
21 20 exlimiv 
 |-  ( E. f f : _om -1-1-> A -> A =/= (/) )
22 1 21 syl 
 |-  ( _om ~<_ A -> A =/= (/) )