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

Theorem snfi 8995
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 8591 . . . 4 1o ∈ ω
2 ensn1g 8970 . . . 4 (𝐴 ∈ V → {𝐴} ≈ 1o)
3 breq2 5114 . . . . 5 (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
43rspcev 3584 . . . 4 ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
51, 2, 4sylancr 588 . . 3 (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6 snprc 4683 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
7 en0 8964 . . . . 5 ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8 peano1 7830 . . . . . 6 ∅ ∈ ω
9 breq2 5114 . . . . . . 7 (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
109rspcev 3584 . . . . . 6 ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
118, 10mpan 689 . . . . 5 ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
127, 11sylbir 234 . . . 4 ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
136, 12sylbi 216 . . 3 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
145, 13pm2.61i 182 . 2 𝑥 ∈ ω {𝐴} ≈ 𝑥
15 isfi 8923 . 2 ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
1614, 15mpbir 230 1 {𝐴} ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1542  wcel 2107  wrex 3074  Vcvv 3448  c0 4287  {csn 4591   class class class wbr 5110  ωcom 7807  1oc1o 8410  cen 8887  Fincfn 8890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-mo 2539  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-om 7808  df-1o 8417  df-en 8891  df-fin 8894
This theorem is referenced by:  fiprc  8996  ssfi  9124  imafi  9126  pwfi  9129  cnvfi  9131  fnfi  9132  sucdom2  9157  prfi  9273  tpfi  9274  unifpw  9306  snopfsupp  9335  sniffsupp  9343  ssfii  9362  cantnfp1lem1  9621  infpwfidom  9971  ficardadju  10142  ackbij1lem4  10166  ackbij1lem9  10171  ackbij1lem10  10172  fin23lem21  10282  isfin1-3  10329  axcclem  10400  zornn0g  10448  hashsng  14276  hashen1  14277  hashunsng  14299  hashunsngx  14300  hashprg  14302  hashsnlei  14325  hashxplem  14340  hashmap  14342  hashfun  14344  hashbclem  14356  hashf1lem1OLD  14361  hashf1lem2  14362  hashf1  14363  fsumsplitsn  15636  fsummsnunz  15646  fsumsplitsnun  15647  fsum2dlem  15662  fsumcom2  15666  ackbijnn  15720  incexclem  15728  isumltss  15740  fprod2dlem  15870  fprodcom2  15874  fprodsplitsn  15879  rexpen  16117  2ebits  16334  lcmfunsnlem2lem1  16521  lcmfunsnlem2lem2  16522  lcmfunsnlem2  16523  lcmfass  16529  phicl2  16647  ramub1lem1  16905  cshwshashnsame  16983  acsfn1  17548  acsfiindd  18449  efmnd1hash  18709  symg1hash  19178  odcau  19393  sylow2alem2  19407  gsumsnfd  19735  gsumzunsnd  19740  gsumunsnfd  19741  gsumpt  19746  ablfac1eu  19859  pgpfaclem2  19868  ablfaclem3  19873  srgbinomlem4  19967  acsfn1p  20282  uvcff  21213  psrlidm  21388  psrridm  21389  mplsubrg  21427  mvrcl  21437  mplmon  21452  mplmonmul  21453  psrbagsn  21487  psr1baslem  21572  mat1dimelbas  21836  mat1dim0  21838  mat1dimid  21839  mat1dimmul  21841  mat1dimcrng  21842  mat1f1o  21843  mat1ghm  21848  mat1mhm  21849  mat1rhm  21850  mat1scmat  21904  mvmumamul1  21919  mdetrsca  21968  mdetunilem9  21985  mdetmul  21988  pmatcoe1fsupp  22066  d1mat2pmat  22104  pmatcollpw3fi1lem1  22151  chpmat1dlem  22200  chpmat1d  22201  0cmp  22761  discmp  22765  bwth  22777  disllycmp  22865  dis1stc  22866  locfincmp  22893  dissnlocfin  22896  comppfsc  22899  1stckgenlem  22920  ptpjpre2  22947  ptopn2  22951  xkohaus  23020  xkoptsub  23021  ptcmpfi  23180  cfinufil  23295  ufinffr  23296  fin1aufil  23299  alexsubALTlem3  23416  ptcmplem5  23423  tmdgsum  23462  tsmsxplem1  23520  tsmsxplem2  23521  prdsmet  23739  imasdsf1olem  23742  prdsbl  23863  icccmplem1  24201  icccmplem2  24202  ovolsn  24875  ovolfiniun  24881  volfiniun  24927  i1f0  25067  fta1glem2  25547  fta1blem  25549  fta1lem  25683  vieta1lem2  25687  vieta1  25688  aalioulem2  25709  tayl0  25737  radcnv0  25791  wilthlem2  26434  fsumvma  26577  dchrfi  26619  cusgrfilem3  28447  eupth2eucrct  29203  trlsegvdeglem7  29212  fusgreghash2wspv  29321  ex-hash  29439  fsupprnfi  31649  ffsrn  31688  fsumiunle  31767  fply1  32305  locfinref  32462  esumcst  32702  esumsnf  32703  hasheuni  32724  rossros  32819  sibf0  32974  eulerpartlems  33000  eulerpartlemb  33008  ccatmulgnn0dir  33194  ofcccat  33195  plymulx0  33199  prodfzo03  33256  breprexp  33286  hgt750lemb  33309  hgt750leme  33311  lpadlem2  33333  derangsn  33804  onsucsuccmpi  34944  topdifinffinlem  35847  pibt2  35917  finixpnum  36092  lindsenlbs  36102  poimirlem26  36133  poimirlem27  36134  poimirlem31  36138  poimirlem32  36139  prdsbnd  36281  heiborlem3  36301  heiborlem8  36306  ismrer1  36326  reheibor  36327  pclfinN  38392  frlmvscadiccat  40710  frlmsnic  40757  evlsbagval  40777  mhphf  40800  elrfi  41046  mzpcompact2lem  41103  dfac11  41418  pwslnmlem0  41447  lpirlnr  41473  mpct  43496  cnrefiisplem  44144  dvmptfprodlem  44259  dvnprodlem2  44262  stoweidlem44  44359  fourierdlem51  44472  fourierdlem80  44501  fouriersw  44546  salexct  44649  salexct3  44657  salgencntex  44658  salgensscntex  44659  sge0sn  44694  sge0tsms  44695  sge0cl  44696  sge0sup  44706  sge0iunmptlemfi  44728  sge0splitsn  44756  hoiprodp1  44903  sge0hsphoire  44904  hoidmv1le  44909  hoidmvlelem1  44910  hoidmvlelem2  44911  hoidmvlelem5  44914  hspmbllem2  44942  ovnovollem3  44973  vonvolmbl  44976  vonvol  44977  vonvol2  44979  fsummmodsnunz  45641  suppmptcfin  46529  lcosn0  46575  lincext2  46610  snlindsntor  46626
  Copyright terms: Public domain W3C validator