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

Theorem snfi 8192
Description: A singleton is finite. (Contributed by NM, 4-Nov-2002.)
Assertion
Ref Expression
snfi {𝐴} ∈ Fin

Proof of Theorem snfi
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 1onn 7871 . . . 4 1𝑜 ∈ ω
2 ensn1g 8172 . . . 4 (𝐴 ∈ V → {𝐴} ≈ 1𝑜)
3 breq2 4787 . . . . 5 (𝑥 = 1𝑜 → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1𝑜))
43rspcev 3457 . . . 4 ((1𝑜 ∈ ω ∧ {𝐴} ≈ 1𝑜) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
51, 2, 4sylancr 695 . . 3 (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6 snprc 4386 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
7 en0 8170 . . . . 5 ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8 peano1 7230 . . . . . 6 ∅ ∈ ω
9 breq2 4787 . . . . . . 7 (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
109rspcev 3457 . . . . . 6 ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
118, 10mpan 705 . . . . 5 ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
127, 11sylbir 225 . . . 4 ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
136, 12sylbi 207 . . 3 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
145, 13pm2.61i 176 . 2 𝑥 ∈ ω {𝐴} ≈ 𝑥
15 isfi 8131 . 2 ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
1614, 15mpbir 221 1 {𝐴} ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1629  wcel 2143  wrex 3060  Vcvv 3348  c0 4060  {csn 4313   class class class wbr 4783  ωcom 7210  1𝑜c1o 7704  cen 8104  Fincfn 8107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2145  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749  ax-sep 4911  ax-nul 4919  ax-pow 4970  ax-pr 5033  ax-un 7094
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1070  df-3an 1071  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-eu 2620  df-mo 2621  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-ne 2942  df-ral 3064  df-rex 3065  df-rab 3068  df-v 3350  df-sbc 3585  df-dif 3723  df-un 3725  df-in 3727  df-ss 3734  df-pss 3736  df-nul 4061  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4572  df-br 4784  df-opab 4844  df-tr 4884  df-id 5156  df-eprel 5161  df-po 5169  df-so 5170  df-fr 5207  df-we 5209  df-xp 5254  df-rel 5255  df-cnv 5256  df-co 5257  df-dm 5258  df-rn 5259  df-res 5260  df-ima 5261  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-om 7211  df-1o 7711  df-en 8108  df-fin 8111
This theorem is referenced by:  fiprc  8193  prfi  8389  tpfi  8390  fnfi  8392  unifpw  8423  snopfsupp  8452  sniffsupp  8469  ssfii  8479  cantnfp1lem1  8737  infpwfidom  9049  ackbij1lem4  9245  ackbij1lem9  9250  ackbij1lem10  9251  fin23lem21  9361  isfin1-3  9408  axcclem  9479  zornn0g  9527  hashsng  13364  hashen1  13365  hashunsng  13386  hashprg  13387  hashprgOLD  13388  hashsnlei  13411  hashxplem  13425  hashmap  13427  hashfun  13429  hashbclem  13441  hashf1lem1  13444  hashf1lem2  13445  hashf1  13446  fsumsplitsn  14685  fsummsnunz  14694  fsumsplitsnun  14695  fsummsnunzOLD  14696  fsumsplitsnunOLD  14697  fsum2dlem  14712  fsumcom2  14716  fsumcom2OLD  14717  ackbijnn  14771  incexclem  14779  isumltss  14791  fprod2dlem  14921  fprodcom2  14925  fprodcom2OLD  14926  fprodsplitsn  14931  rexpen  15168  2ebits  15383  lcmfunsnlem2lem1  15565  lcmfunsnlem2lem2  15566  lcmfunsnlem2  15567  lcmfass  15573  phicl2  15686  ramub1lem1  15943  cshwshashnsame  16023  acsfn1  16535  acsfiindd  17391  symg1hash  18028  odcau  18232  sylow2alem2  18246  gsumsnfd  18564  gsumzunsnd  18568  gsumunsnfd  18569  gsumpt  18574  ablfac1eu  18686  pgpfaclem2  18695  ablfaclem3  18700  srgbinomlem4  18757  psrlidm  19624  psrridm  19625  mplsubrg  19661  mvrcl  19670  mplmon  19684  mplmonmul  19685  psrbagsn  19716  psr1baslem  19776  uvcff  20353  mat1dimelbas  20501  mat1dim0  20503  mat1dimid  20504  mat1dimmul  20506  mat1dimcrng  20507  mat1f1o  20508  mat1ghm  20513  mat1mhm  20514  mat1rhm  20515  mat1rngiso  20516  mat1scmat  20569  mvmumamul1  20584  mdetrsca  20633  mdetunilem9  20650  mdetmul  20653  pmatcoe1fsupp  20732  d1mat2pmat  20770  pmatcollpw3fi1lem1  20817  chpmat1dlem  20866  chpmat1d  20867  0cmp  21424  discmp  21428  bwth  21440  disllycmp  21528  dis1stc  21529  locfincmp  21556  dissnlocfin  21559  comppfsc  21562  1stckgenlem  21583  ptpjpre2  21610  ptopn2  21614  xkohaus  21683  xkoptsub  21684  ptcmpfi  21843  cfinufil  21958  ufinffr  21959  fin1aufil  21962  alexsubALTlem3  22079  ptcmplem5  22086  tmdgsum  22125  tsmsxplem1  22182  tsmsxplem2  22183  prdsmet  22401  imasdsf1olem  22404  prdsbl  22522  icccmplem1  22851  icccmplem2  22852  ovolsn  23489  ovolfiniun  23495  volfiniun  23541  i1f0  23680  fta1glem2  24152  fta1blem  24154  fta1lem  24288  vieta1lem2  24292  vieta1  24293  aalioulem2  24314  tayl0  24342  radcnv0  24396  wilthlem2  25022  fsumvma  25165  dchrfi  25207  cusgrfilem3  26594  eupth2eucrct  27401  trlsegvdeglem7  27410  fusgreghash2wspv  27521  ex-hash  27653  ffsrn  29845  fsumiunle  29916  locfinref  30249  esumcst  30466  esumsnf  30467  hasheuni  30488  rossros  30584  sibf0  30737  eulerpartlems  30763  eulerpartlemb  30771  ccatmulgnn0dir  30960  ofcccat  30961  plymulx0  30965  prodfzo03  31022  breprexp  31052  hgt750lemb  31075  hgt750leme  31077  derangsn  31491  onsucsuccmpi  32780  topdifinffinlem  33532  finixpnum  33727  lindsenlbs  33737  poimirlem26  33768  poimirlem27  33769  poimirlem31  33773  poimirlem32  33774  prdsbnd  33924  heiborlem3  33944  heiborlem8  33949  ismrer1  33969  reheibor  33970  pclfinN  35708  elrfi  37783  mzpcompact2lem  37840  dfac11  38158  pwslnmlem0  38187  lpirlnr  38213  acsfn1p  38295  mpct  39912  cnrefiisplem  40574  dvmptfprodlem  40678  dvnprodlem2  40681  stoweidlem44  40779  fourierdlem51  40892  fourierdlem80  40921  fouriersw  40966  salexct  41070  salexct3  41078  salgencntex  41079  salgensscntex  41080  sge0sn  41114  sge0tsms  41115  sge0cl  41116  sge0sup  41126  sge0iunmptlemfi  41148  sge0splitsn  41176  hoiprodp1  41323  sge0hsphoire  41324  hoidmv1le  41329  hoidmvlelem1  41330  hoidmvlelem2  41331  hoidmvlelem5  41334  hspmbllem2  41362  ovnovollem3  41393  vonvolmbl  41396  vonvol  41397  vonvol2  41399  fsummmodsnunz  41870  suppmptcfin  42685  lcosn0  42734  lincext2  42769  snlindsntor  42785
  Copyright terms: Public domain W3C validator