MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  infn0 Structured version   Visualization version   GIF version

Theorem infn0 9332
Description: An infinite set is not empty. For a shorter proof using ax-un 7740, see infn0ALT 9333. (Contributed by NM, 23-Oct-2004.) Avoid ax-un 7740. (Revised by BTernaryTau, 8-Jan-2025.)
Assertion
Ref Expression
infn0 (Ο‰ β‰Ό 𝐴 β†’ 𝐴 β‰  βˆ…)

Proof of Theorem infn0
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 brdomi 8979 . 2 (Ο‰ β‰Ό 𝐴 β†’ βˆƒπ‘“ 𝑓:ω–1-1→𝐴)
2 peano1 7894 . . . . . 6 βˆ… ∈ Ο‰
3 f1f1orn 6850 . . . . . . . . 9 (𝑓:ω–1-1→𝐴 β†’ 𝑓:ω–1-1-ontoβ†’ran 𝑓)
43adantr 480 . . . . . . . 8 ((𝑓:ω–1-1→𝐴 ∧ 𝐴 = βˆ…) β†’ 𝑓:ω–1-1-ontoβ†’ran 𝑓)
5 f1f 6793 . . . . . . . . . . 11 (𝑓:ω–1-1→𝐴 β†’ 𝑓:Ο‰βŸΆπ΄)
65frnd 6730 . . . . . . . . . 10 (𝑓:ω–1-1→𝐴 β†’ ran 𝑓 βŠ† 𝐴)
7 sseq0 4400 . . . . . . . . . 10 ((ran 𝑓 βŠ† 𝐴 ∧ 𝐴 = βˆ…) β†’ ran 𝑓 = βˆ…)
86, 7sylan 579 . . . . . . . . 9 ((𝑓:ω–1-1→𝐴 ∧ 𝐴 = βˆ…) β†’ ran 𝑓 = βˆ…)
98f1oeq3d 6836 . . . . . . . 8 ((𝑓:ω–1-1→𝐴 ∧ 𝐴 = βˆ…) β†’ (𝑓:ω–1-1-ontoβ†’ran 𝑓 ↔ 𝑓:ω–1-1-ontoβ†’βˆ…))
104, 9mpbid 231 . . . . . . 7 ((𝑓:ω–1-1→𝐴 ∧ 𝐴 = βˆ…) β†’ 𝑓:ω–1-1-ontoβ†’βˆ…)
11 f1ocnv 6851 . . . . . . 7 (𝑓:ω–1-1-ontoβ†’βˆ… β†’ ◑𝑓:βˆ…β€“1-1-ontoβ†’Ο‰)
12 noel 4331 . . . . . . . 8 Β¬ βˆ… ∈ βˆ…
13 f1o00 6874 . . . . . . . . . 10 (◑𝑓:βˆ…β€“1-1-ontoβ†’Ο‰ ↔ (◑𝑓 = βˆ… ∧ Ο‰ = βˆ…))
1413simprbi 496 . . . . . . . . 9 (◑𝑓:βˆ…β€“1-1-ontoβ†’Ο‰ β†’ Ο‰ = βˆ…)
1514eleq2d 2815 . . . . . . . 8 (◑𝑓:βˆ…β€“1-1-ontoβ†’Ο‰ β†’ (βˆ… ∈ Ο‰ ↔ βˆ… ∈ βˆ…))
1612, 15mtbiri 327 . . . . . . 7 (◑𝑓:βˆ…β€“1-1-ontoβ†’Ο‰ β†’ Β¬ βˆ… ∈ Ο‰)
1710, 11, 163syl 18 . . . . . 6 ((𝑓:ω–1-1→𝐴 ∧ 𝐴 = βˆ…) β†’ Β¬ βˆ… ∈ Ο‰)
182, 17mt2 199 . . . . 5 Β¬ (𝑓:ω–1-1→𝐴 ∧ 𝐴 = βˆ…)
1918imnani 400 . . . 4 (𝑓:ω–1-1→𝐴 β†’ Β¬ 𝐴 = βˆ…)
2019neqned 2944 . . 3 (𝑓:ω–1-1→𝐴 β†’ 𝐴 β‰  βˆ…)
2120exlimiv 1926 . 2 (βˆƒπ‘“ 𝑓:ω–1-1→𝐴 β†’ 𝐴 β‰  βˆ…)
221, 21syl 17 1 (Ο‰ β‰Ό 𝐴 β†’ 𝐴 β‰  βˆ…)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   = wceq 1534  βˆƒwex 1774   ∈ wcel 2099   β‰  wne 2937   βŠ† wss 3947  βˆ…c0 4323   class class class wbr 5148  β—‘ccnv 5677  ran crn 5679  β€“1-1β†’wf1 6545  β€“1-1-ontoβ†’wf1o 6547  Ο‰com 7870   β‰Ό cdom 8962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-mo 2530  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-ord 6372  df-on 6373  df-lim 6374  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-om 7871  df-dom 8966
This theorem is referenced by:  infpwfien  10086  infxp  10239  infpss  10241  alephmul  10602  csdfil  23811
  Copyright terms: Public domain W3C validator