Theorem snfi 8843

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.

Step	Hyp	Ref	Expression
1		1onn 8479	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8818	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5079	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3562	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		snprc 4654	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
7		en0 8812	. . . . 5 ⊢ ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8		peano1 7744	. . . . . 6 ⊢ ∅ ∈ ω
9		breq2 5079	. . . . . . 7 ⊢ (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
10	9	rspcev 3562	. . . . . 6 ⊢ ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
11	8, 10	mpan 687	. . . . 5 ⊢ ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
12	7, 11	sylbir 234	. . . 4 ⊢ ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
13	6, 12	sylbi 216	. . 3 ⊢ (¬ 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
14	5, 13	pm2.61i 182	. 2 ⊢ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥
15		isfi 8773	. 2 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
16	14, 15	mpbir 230	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2107  ∃wrex 3066  Vcvv 3433  ∅c0 4257  {csn 4562   class class class wbr 5075  ωcom 7721  1_oc1o 8299   ≈ cen 8739  Fincfn 8742

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-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-mo 2541  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-om 7722  df-1o 8306  df-en 8743  df-fin 8746

This theorem is referenced by:  fiprc  8844  ssfi  8965  imafi  8967  pwfi  8970  cnvfi  8972  fnfi  8973  sucdom2  8998  prfi  9098  tpfi  9099  unifpw  9131  snopfsupp  9160  sniffsupp  9168  ssfii  9187  cantnfp1lem1  9445  infpwfidom  9793  ficardadju  9964  ackbij1lem4  9988  ackbij1lem9  9993  ackbij1lem10  9994  fin23lem21  10104  isfin1-3  10151  axcclem  10222  zornn0g  10270  hashsng  14093  hashen1  14094  hashunsng  14116  hashunsngx  14117  hashprg  14119  hashsnlei  14142  hashxplem  14157  hashmap  14159  hashfun  14161  hashbclem  14173  hashf1lem1OLD  14178  hashf1lem2  14179  hashf1  14180  fsumsplitsn  15465  fsummsnunz  15475  fsumsplitsnun  15476  fsum2dlem  15491  fsumcom2  15495  ackbijnn  15549  incexclem  15557  isumltss  15569  fprod2dlem  15699  fprodcom2  15703  fprodsplitsn  15708  rexpen  15946  2ebits  16163  lcmfunsnlem2lem1  16352  lcmfunsnlem2lem2  16353  lcmfunsnlem2  16354  lcmfass  16360  phicl2  16478  ramub1lem1  16736  cshwshashnsame  16814  acsfn1  17379  acsfiindd  18280  efmnd1hash  18540  symg1hash  19006  odcau  19218  sylow2alem2  19232  gsumsnfd  19561  gsumzunsnd  19566  gsumunsnfd  19567  gsumpt  19572  ablfac1eu  19685  pgpfaclem2  19694  ablfaclem3  19699  srgbinomlem4  19788  acsfn1p  20076  uvcff  21007  psrlidm  21181  psrridm  21182  mplsubrg  21220  mvrcl  21230  mplmon  21245  mplmonmul  21246  psrbagsn  21280  psr1baslem  21365  mat1dimelbas  21629  mat1dim0  21631  mat1dimid  21632  mat1dimmul  21634  mat1dimcrng  21635  mat1f1o  21636  mat1ghm  21641  mat1mhm  21642  mat1rhm  21643  mat1rngiso  21644  mat1scmat  21697  mvmumamul1  21712  mdetrsca  21761  mdetunilem9  21778  mdetmul  21781  pmatcoe1fsupp  21859  d1mat2pmat  21897  pmatcollpw3fi1lem1  21944  chpmat1dlem  21993  chpmat1d  21994  0cmp  22554  discmp  22558  bwth  22570  disllycmp  22658  dis1stc  22659  locfincmp  22686  dissnlocfin  22689  comppfsc  22692  1stckgenlem  22713  ptpjpre2  22740  ptopn2  22744  xkohaus  22813  xkoptsub  22814  ptcmpfi  22973  cfinufil  23088  ufinffr  23089  fin1aufil  23092  alexsubALTlem3  23209  ptcmplem5  23216  tmdgsum  23255  tsmsxplem1  23313  tsmsxplem2  23314  prdsmet  23532  imasdsf1olem  23535  prdsbl  23656  icccmplem1  23994  icccmplem2  23995  ovolsn  24668  ovolfiniun  24674  volfiniun  24720  i1f0  24860  fta1glem2  25340  fta1blem  25342  fta1lem  25476  vieta1lem2  25480  vieta1  25481  aalioulem2  25502  tayl0  25530  radcnv0  25584  wilthlem2  26227  fsumvma  26370  dchrfi  26412  cusgrfilem3  27833  eupth2eucrct  28590  trlsegvdeglem7  28599  fusgreghash2wspv  28708  ex-hash  28826  fsupprnfi  31035  ffsrn  31073  fsumiunle  31152  fply1  31676  locfinref  31800  esumcst  32040  esumsnf  32041  hasheuni  32062  rossros  32157  sibf0  32310  eulerpartlems  32336  eulerpartlemb  32344  ccatmulgnn0dir  32530  ofcccat  32531  plymulx0  32535  prodfzo03  32592  breprexp  32622  hgt750lemb  32645  hgt750leme  32647  lpadlem2  32669  derangsn  33141  onsucsuccmpi  34641  topdifinffinlem  35527  pibt2  35597  finixpnum  35771  lindsenlbs  35781  poimirlem26  35812  poimirlem27  35813  poimirlem31  35817  poimirlem32  35818  prdsbnd  35960  heiborlem3  35980  heiborlem8  35985  ismrer1  36005  reheibor  36006  pclfinN  37921  frlmvscadiccat  40244  frlmsnic  40270  evlsbagval  40282  mhphf  40292  elrfi  40523  mzpcompact2lem  40580  dfac11  40894  pwslnmlem0  40923  lpirlnr  40949  mpct  42748  cnrefiisplem  43377  dvmptfprodlem  43492  dvnprodlem2  43495  stoweidlem44  43592  fourierdlem51  43705  fourierdlem80  43734  fouriersw  43779  salexct  43880  salexct3  43888  salgencntex  43889  salgensscntex  43890  sge0sn  43924  sge0tsms  43925  sge0cl  43926  sge0sup  43936  sge0iunmptlemfi  43958  sge0splitsn  43986  hoiprodp1  44133  sge0hsphoire  44134  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem5  44144  hspmbllem2  44172  ovnovollem3  44203  vonvolmbl  44206  vonvol  44207  vonvol2  44209  fsummmodsnunz  44838  suppmptcfin  45726  lcosn0  45772  lincext2  45807  snlindsntor  45823