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 =/= (/) )