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

Proof

Step Hyp Ref Expression
1 brdomi ω A f f : ω 1-1 A
2 peano1 ω
3 f1f1orn f : ω 1-1 A f : ω 1-1 onto ran f
4 3 adantr f : ω 1-1 A A = f : ω 1-1 onto ran f
5 f1f f : ω 1-1 A f : ω A
6 5 frnd f : ω 1-1 A ran f A
7 sseq0 ran f A A = ran f =
8 6 7 sylan f : ω 1-1 A A = ran f =
9 8 f1oeq3d f : ω 1-1 A A = f : ω 1-1 onto ran f f : ω 1-1 onto
10 4 9 mpbid f : ω 1-1 A A = f : ω 1-1 onto
11 f1ocnv f : ω 1-1 onto f -1 : 1-1 onto ω
12 noel ¬
13 f1o00 f -1 : 1-1 onto ω f -1 = ω =
14 13 simprbi f -1 : 1-1 onto ω ω =
15 14 eleq2d f -1 : 1-1 onto ω ω
16 12 15 mtbiri f -1 : 1-1 onto ω ¬ ω
17 10 11 16 3syl f : ω 1-1 A A = ¬ ω
18 2 17 mt2 ¬ f : ω 1-1 A A =
19 18 imnani f : ω 1-1 A ¬ A =
20 19 neqned f : ω 1-1 A A
21 20 exlimiv f f : ω 1-1 A A
22 1 21 syl ω A A