Theorem snfi 8901

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 8533	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8876	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5093	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3570	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		snprc 4664	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
7		en0 8870	. . . . 5 ⊢ ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8		peano1 7795	. . . . . 6 ⊢ ∅ ∈ ω
9		breq2 5093	. . . . . . 7 ⊢ (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
10	9	rspcev 3570	. . . . . 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 8829	. 2 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
16	14, 15	mpbir 230	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2105  ∃wrex 3070  Vcvv 3441  ∅c0 4268  {csn 4572   class class class wbr 5089  ωcom 7772  1_oc1o 8352   ≈ cen 8793  Fincfn 8796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pr 5369

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-mo 2538  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-om 7773  df-1o 8359  df-en 8797  df-fin 8800

This theorem is referenced by:  fiprc  8902  ssfi  9030  imafi  9032  pwfi  9035  cnvfi  9037  fnfi  9038  sucdom2  9063  prfi  9179  tpfi  9180  unifpw  9212  snopfsupp  9241  sniffsupp  9249  ssfii  9268  cantnfp1lem1  9527  infpwfidom  9877  ficardadju  10048  ackbij1lem4  10072  ackbij1lem9  10077  ackbij1lem10  10078  fin23lem21  10188  isfin1-3  10235  axcclem  10306  zornn0g  10354  hashsng  14176  hashen1  14177  hashunsng  14199  hashunsngx  14200  hashprg  14202  hashsnlei  14225  hashxplem  14240  hashmap  14242  hashfun  14244  hashbclem  14256  hashf1lem1OLD  14261  hashf1lem2  14262  hashf1  14263  fsumsplitsn  15547  fsummsnunz  15557  fsumsplitsnun  15558  fsum2dlem  15573  fsumcom2  15577  ackbijnn  15631  incexclem  15639  isumltss  15651  fprod2dlem  15781  fprodcom2  15785  fprodsplitsn  15790  rexpen  16028  2ebits  16245  lcmfunsnlem2lem1  16432  lcmfunsnlem2lem2  16433  lcmfunsnlem2  16434  lcmfass  16440  phicl2  16558  ramub1lem1  16816  cshwshashnsame  16894  acsfn1  17459  acsfiindd  18360  efmnd1hash  18619  symg1hash  19085  odcau  19297  sylow2alem2  19311  gsumsnfd  19639  gsumzunsnd  19644  gsumunsnfd  19645  gsumpt  19650  ablfac1eu  19763  pgpfaclem2  19772  ablfaclem3  19777  srgbinomlem4  19866  acsfn1p  20165  uvcff  21096  psrlidm  21270  psrridm  21271  mplsubrg  21309  mvrcl  21319  mplmon  21334  mplmonmul  21335  psrbagsn  21369  psr1baslem  21454  mat1dimelbas  21718  mat1dim0  21720  mat1dimid  21721  mat1dimmul  21723  mat1dimcrng  21724  mat1f1o  21725  mat1ghm  21730  mat1mhm  21731  mat1rhm  21732  mat1scmat  21786  mvmumamul1  21801  mdetrsca  21850  mdetunilem9  21867  mdetmul  21870  pmatcoe1fsupp  21948  d1mat2pmat  21986  pmatcollpw3fi1lem1  22033  chpmat1dlem  22082  chpmat1d  22083  0cmp  22643  discmp  22647  bwth  22659  disllycmp  22747  dis1stc  22748  locfincmp  22775  dissnlocfin  22778  comppfsc  22781  1stckgenlem  22802  ptpjpre2  22829  ptopn2  22833  xkohaus  22902  xkoptsub  22903  ptcmpfi  23062  cfinufil  23177  ufinffr  23178  fin1aufil  23181  alexsubALTlem3  23298  ptcmplem5  23305  tmdgsum  23344  tsmsxplem1  23402  tsmsxplem2  23403  prdsmet  23621  imasdsf1olem  23624  prdsbl  23745  icccmplem1  24083  icccmplem2  24084  ovolsn  24757  ovolfiniun  24763  volfiniun  24809  i1f0  24949  fta1glem2  25429  fta1blem  25431  fta1lem  25565  vieta1lem2  25569  vieta1  25570  aalioulem2  25591  tayl0  25619  radcnv0  25673  wilthlem2  26316  fsumvma  26459  dchrfi  26501  cusgrfilem3  28054  eupth2eucrct  28810  trlsegvdeglem7  28819  fusgreghash2wspv  28928  ex-hash  29046  fsupprnfi  31254  ffsrn  31292  fsumiunle  31371  fply1  31905  locfinref  32030  esumcst  32270  esumsnf  32271  hasheuni  32292  rossros  32387  sibf0  32542  eulerpartlems  32568  eulerpartlemb  32576  ccatmulgnn0dir  32762  ofcccat  32763  plymulx0  32767  prodfzo03  32824  breprexp  32854  hgt750lemb  32877  hgt750leme  32879  lpadlem2  32901  derangsn  33372  onsucsuccmpi  34723  topdifinffinlem  35616  pibt2  35686  finixpnum  35860  lindsenlbs  35870  poimirlem26  35901  poimirlem27  35902  poimirlem31  35906  poimirlem32  35907  prdsbnd  36049  heiborlem3  36069  heiborlem8  36074  ismrer1  36094  reheibor  36095  pclfinN  38161  frlmvscadiccat  40484  frlmsnic  40513  evlsbagval  40525  mhphf  40535  elrfi  40766  mzpcompact2lem  40823  dfac11  41138  pwslnmlem0  41167  lpirlnr  41193  mpct  43057  cnrefiisplem  43695  dvmptfprodlem  43810  dvnprodlem2  43813  stoweidlem44  43910  fourierdlem51  44023  fourierdlem80  44052  fouriersw  44097  salexct  44198  salexct3  44206  salgencntex  44207  salgensscntex  44208  sge0sn  44243  sge0tsms  44244  sge0cl  44245  sge0sup  44255  sge0iunmptlemfi  44277  sge0splitsn  44305  hoiprodp1  44452  sge0hsphoire  44453  hoidmv1le  44458  hoidmvlelem1  44459  hoidmvlelem2  44460  hoidmvlelem5  44463  hspmbllem2  44491  ovnovollem3  44522  vonvolmbl  44525  vonvol  44526  vonvol2  44528  fsummmodsnunz  45167  suppmptcfin  46055  lcosn0  46101  lincext2  46136  snlindsntor  46152