Theorem snfi 8449

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 8122	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8429	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 4972	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3561	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		snprc 4566	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
7		en0 8427	. . . . 5 ⊢ ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8		peano1 7464	. . . . . 6 ⊢ ∅ ∈ ω
9		breq2 4972	. . . . . . 7 ⊢ (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
10	9	rspcev 3561	. . . . . 6 ⊢ ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
11	8, 10	mpan 686	. . . . 5 ⊢ ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
12	7, 11	sylbir 236	. . . 4 ⊢ ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
13	6, 12	sylbi 218	. . 3 ⊢ (¬ 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
14	5, 13	pm2.61i 183	. 2 ⊢ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥
15		isfi 8388	. 2 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
16	14, 15	mpbir 232	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1525   ∈ wcel 2083  ∃wrex 3108  Vcvv 3440  ∅c0 4217  {csn 4478   class class class wbr 4968  ωcom 7443  1_oc1o 7953   ≈ cen 8361  Fincfn 8364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-om 7444  df-1o 7960  df-en 8365  df-fin 8368

This theorem is referenced by:  fiprc  8450  prfi  8646  tpfi  8647  fnfi  8649  unifpw  8680  snopfsupp  8709  sniffsupp  8726  ssfii  8736  cantnfp1lem1  8994  infpwfidom  9307  ackbij1lem4  9498  ackbij1lem9  9503  ackbij1lem10  9504  fin23lem21  9614  isfin1-3  9661  axcclem  9732  zornn0g  9780  hashsng  13583  hashen1  13584  hashunsng  13605  hashunsngx  13606  hashprg  13608  hashsnlei  13631  hashxplem  13646  hashmap  13648  hashfun  13650  hashbclem  13662  hashf1lem1  13665  hashf1lem2  13666  hashf1  13667  fsumsplitsn  14937  fsummsnunz  14946  fsumsplitsnun  14947  fsum2dlem  14962  fsumcom2  14966  ackbijnn  15020  incexclem  15028  isumltss  15040  fprod2dlem  15171  fprodcom2  15175  fprodsplitsn  15180  rexpen  15418  2ebits  15633  lcmfunsnlem2lem1  15815  lcmfunsnlem2lem2  15816  lcmfunsnlem2  15817  lcmfass  15823  phicl2  15938  ramub1lem1  16195  cshwshashnsame  16270  acsfn1  16765  acsfiindd  17620  symg1hash  18258  odcau  18463  sylow2alem2  18477  gsumsnfd  18795  gsumzunsnd  18800  gsumunsnfd  18801  gsumpt  18806  ablfac1eu  18916  pgpfaclem2  18925  ablfaclem3  18930  srgbinomlem4  18987  acsfn1p  19272  psrlidm  19875  psrridm  19876  mplsubrg  19912  mvrcl  19921  mplmon  19935  mplmonmul  19936  psrbagsn  19966  psr1baslem  20040  uvcff  20621  mat1dimelbas  20768  mat1dim0  20770  mat1dimid  20771  mat1dimmul  20773  mat1dimcrng  20774  mat1f1o  20775  mat1ghm  20780  mat1mhm  20781  mat1rhm  20782  mat1rngiso  20783  mat1scmat  20836  mvmumamul1  20851  mdetrsca  20900  mdetunilem9  20917  mdetmul  20920  pmatcoe1fsupp  20997  d1mat2pmat  21035  pmatcollpw3fi1lem1  21082  chpmat1dlem  21131  chpmat1d  21132  0cmp  21690  discmp  21694  bwth  21706  disllycmp  21794  dis1stc  21795  locfincmp  21822  dissnlocfin  21825  comppfsc  21828  1stckgenlem  21849  ptpjpre2  21876  ptopn2  21880  xkohaus  21949  xkoptsub  21950  ptcmpfi  22109  cfinufil  22224  ufinffr  22225  fin1aufil  22228  alexsubALTlem3  22345  ptcmplem5  22352  tmdgsum  22391  tsmsxplem1  22448  tsmsxplem2  22449  prdsmet  22667  imasdsf1olem  22670  prdsbl  22788  icccmplem1  23117  icccmplem2  23118  ovolsn  23783  ovolfiniun  23789  volfiniun  23835  i1f0  23975  fta1glem2  24447  fta1blem  24449  fta1lem  24583  vieta1lem2  24587  vieta1  24588  aalioulem2  24609  tayl0  24637  radcnv0  24691  wilthlem2  25332  fsumvma  25475  dchrfi  25517  cusgrfilem3  26926  eupth2eucrct  27682  trlsegvdeglem7  27691  fusgreghash2wspv  27802  ex-hash  27920  ffsrn  30149  fsumiunle  30225  fply1  30575  locfinref  30718  esumcst  30935  esumsnf  30936  hasheuni  30957  rossros  31052  sibf0  31205  eulerpartlems  31231  eulerpartlemb  31239  ccatmulgnn0dir  31425  ofcccat  31426  plymulx0  31430  prodfzo03  31487  breprexp  31517  hgt750lemb  31540  hgt750leme  31542  lpadlem2  31564  derangsn  32027  onsucsuccmpi  33402  topdifinffinlem  34180  pibt2  34250  finixpnum  34429  lindsenlbs  34439  poimirlem26  34470  poimirlem27  34471  poimirlem31  34475  poimirlem32  34476  prdsbnd  34624  heiborlem3  34644  heiborlem8  34649  ismrer1  34669  reheibor  34670  pclfinN  36588  frlmvscadiccat  38693  frlmsnic  38697  elrfi  38797  mzpcompact2lem  38854  dfac11  39168  pwslnmlem0  39197  lpirlnr  39223  mpct  41025  cnrefiisplem  41673  dvmptfprodlem  41792  dvnprodlem2  41795  stoweidlem44  41893  fourierdlem51  42006  fourierdlem80  42035  fouriersw  42080  salexct  42181  salexct3  42189  salgencntex  42190  salgensscntex  42191  sge0sn  42225  sge0tsms  42226  sge0cl  42227  sge0sup  42237  sge0iunmptlemfi  42259  sge0splitsn  42287  hoiprodp1  42434  sge0hsphoire  42435  hoidmv1le  42440  hoidmvlelem1  42441  hoidmvlelem2  42442  hoidmvlelem5  42445  hspmbllem2  42473  ovnovollem3  42504  vonvolmbl  42507  vonvol  42508  vonvol2  42510  fsummmodsnunz  43073  suppmptcfin  43929  lcosn0  43977  lincext2  44012  snlindsntor  44028