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

Theorem infn0 9304
Description: An infinite set is not empty. For a shorter proof using ax-un 7719, see infn0ALT 9305. (Contributed by NM, 23-Oct-2004.) Avoid ax-un 7719. (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 8951 . 2 (Ο‰ β‰Ό 𝐴 β†’ βˆƒπ‘“ 𝑓:ω–1-1→𝐴)
2 peano1 7873 . . . . . 6 βˆ… ∈ Ο‰
3 f1f1orn 6835 . . . . . . . . 9 (𝑓:ω–1-1→𝐴 β†’ 𝑓:ω–1-1-ontoβ†’ran 𝑓)
43adantr 480 . . . . . . . 8 ((𝑓:ω–1-1→𝐴 ∧ 𝐴 = βˆ…) β†’ 𝑓:ω–1-1-ontoβ†’ran 𝑓)
5 f1f 6778 . . . . . . . . . . 11 (𝑓:ω–1-1→𝐴 β†’ 𝑓:Ο‰βŸΆπ΄)
65frnd 6716 . . . . . . . . . 10 (𝑓:ω–1-1→𝐴 β†’ ran 𝑓 βŠ† 𝐴)
7 sseq0 4392 . . . . . . . . . 10 ((ran 𝑓 βŠ† 𝐴 ∧ 𝐴 = βˆ…) β†’ ran 𝑓 = βˆ…)
86, 7sylan 579 . . . . . . . . 9 ((𝑓:ω–1-1→𝐴 ∧ 𝐴 = βˆ…) β†’ ran 𝑓 = βˆ…)
98f1oeq3d 6821 . . . . . . . 8 ((𝑓:ω–1-1→𝐴 ∧ 𝐴 = βˆ…) β†’ (𝑓:ω–1-1-ontoβ†’ran 𝑓 ↔ 𝑓:ω–1-1-ontoβ†’βˆ…))
104, 9mpbid 231 . . . . . . 7 ((𝑓:ω–1-1→𝐴 ∧ 𝐴 = βˆ…) β†’ 𝑓:ω–1-1-ontoβ†’βˆ…)
11 f1ocnv 6836 . . . . . . 7 (𝑓:ω–1-1-ontoβ†’βˆ… β†’ ◑𝑓:βˆ…β€“1-1-ontoβ†’Ο‰)
12 noel 4323 . . . . . . . 8 Β¬ βˆ… ∈ βˆ…
13 f1o00 6859 . . . . . . . . . 10 (◑𝑓:βˆ…β€“1-1-ontoβ†’Ο‰ ↔ (◑𝑓 = βˆ… ∧ Ο‰ = βˆ…))
1413simprbi 496 . . . . . . . . 9 (◑𝑓:βˆ…β€“1-1-ontoβ†’Ο‰ β†’ Ο‰ = βˆ…)
1514eleq2d 2811 . . . . . . . 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 2939 . . 3 (𝑓:ω–1-1→𝐴 β†’ 𝐴 β‰  βˆ…)
2120exlimiv 1925 . 2 (βˆƒπ‘“ 𝑓:ω–1-1→𝐴 β†’ 𝐴 β‰  βˆ…)
221, 21syl 17 1 (Ο‰ β‰Ό 𝐴 β†’ 𝐴 β‰  βˆ…)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2932   βŠ† wss 3941  βˆ…c0 4315   class class class wbr 5139  β—‘ccnv 5666  ran crn 5668  β€“1-1β†’wf1 6531  β€“1-1-ontoβ†’wf1o 6533  Ο‰com 7849   β‰Ό cdom 8934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-mo 2526  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-ord 6358  df-on 6359  df-lim 6360  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-om 7850  df-dom 8938
This theorem is referenced by:  infpwfien  10054  infxp  10207  infpss  10209  alephmul  10570  csdfil  23742
  Copyright terms: Public domain W3C validator