Theorem snfi 8699

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 8345	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8674	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5043	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3527	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 590	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		snprc 4619	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
7		en0 8669	. . . . 5 ⊢ ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8		peano1 7645	. . . . . 6 ⊢ ∅ ∈ ω
9		breq2 5043	. . . . . . 7 ⊢ (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
10	9	rspcev 3527	. . . . . 6 ⊢ ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
11	8, 10	mpan 690	. . . . 5 ⊢ ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
12	7, 11	sylbir 238	. . . 4 ⊢ ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
13	6, 12	sylbi 220	. . 3 ⊢ (¬ 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
14	5, 13	pm2.61i 185	. 2 ⊢ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥
15		isfi 8630	. 2 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
16	14, 15	mpbir 234	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1543   ∈ wcel 2112  ∃wrex 3052  Vcvv 3398  ∅c0 4223  {csn 4527   class class class wbr 5039  ωcom 7622  1_oc1o 8173   ≈ cen 8601  Fincfn 8604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-om 7623  df-1o 8180  df-en 8605  df-fin 8608

This theorem is referenced by:  fiprc  8700  ssfi  8829  imafi  8830  pwfi  8833  cnvfi  8834  fnfi  8835  prfi  8924  tpfi  8925  unifpw  8957  snopfsupp  8986  sniffsupp  8994  ssfii  9013  cantnfp1lem1  9271  infpwfidom  9607  ficardadju  9778  ackbij1lem4  9802  ackbij1lem9  9807  ackbij1lem10  9808  fin23lem21  9918  isfin1-3  9965  axcclem  10036  zornn0g  10084  hashsng  13901  hashen1  13902  hashunsng  13924  hashunsngx  13925  hashprg  13927  hashsnlei  13950  hashxplem  13965  hashmap  13967  hashfun  13969  hashbclem  13981  hashf1lem1OLD  13986  hashf1lem2  13987  hashf1  13988  fsumsplitsn  15272  fsummsnunz  15281  fsumsplitsnun  15282  fsum2dlem  15297  fsumcom2  15301  ackbijnn  15355  incexclem  15363  isumltss  15375  fprod2dlem  15505  fprodcom2  15509  fprodsplitsn  15514  rexpen  15752  2ebits  15969  lcmfunsnlem2lem1  16158  lcmfunsnlem2lem2  16159  lcmfunsnlem2  16160  lcmfass  16166  phicl2  16284  ramub1lem1  16542  cshwshashnsame  16620  acsfn1  17118  acsfiindd  18013  efmnd1hash  18273  symg1hash  18736  odcau  18947  sylow2alem2  18961  gsumsnfd  19290  gsumzunsnd  19295  gsumunsnfd  19296  gsumpt  19301  ablfac1eu  19414  pgpfaclem2  19423  ablfaclem3  19428  srgbinomlem4  19512  acsfn1p  19797  uvcff  20707  psrlidm  20882  psrridm  20883  mplsubrg  20921  mvrcl  20931  mplmon  20946  mplmonmul  20947  psrbagsn  20975  psr1baslem  21060  mat1dimelbas  21322  mat1dim0  21324  mat1dimid  21325  mat1dimmul  21327  mat1dimcrng  21328  mat1f1o  21329  mat1ghm  21334  mat1mhm  21335  mat1rhm  21336  mat1rngiso  21337  mat1scmat  21390  mvmumamul1  21405  mdetrsca  21454  mdetunilem9  21471  mdetmul  21474  pmatcoe1fsupp  21552  d1mat2pmat  21590  pmatcollpw3fi1lem1  21637  chpmat1dlem  21686  chpmat1d  21687  0cmp  22245  discmp  22249  bwth  22261  disllycmp  22349  dis1stc  22350  locfincmp  22377  dissnlocfin  22380  comppfsc  22383  1stckgenlem  22404  ptpjpre2  22431  ptopn2  22435  xkohaus  22504  xkoptsub  22505  ptcmpfi  22664  cfinufil  22779  ufinffr  22780  fin1aufil  22783  alexsubALTlem3  22900  ptcmplem5  22907  tmdgsum  22946  tsmsxplem1  23004  tsmsxplem2  23005  prdsmet  23222  imasdsf1olem  23225  prdsbl  23343  icccmplem1  23673  icccmplem2  23674  ovolsn  24346  ovolfiniun  24352  volfiniun  24398  i1f0  24538  fta1glem2  25018  fta1blem  25020  fta1lem  25154  vieta1lem2  25158  vieta1  25159  aalioulem2  25180  tayl0  25208  radcnv0  25262  wilthlem2  25905  fsumvma  26048  dchrfi  26090  cusgrfilem3  27499  eupth2eucrct  28254  trlsegvdeglem7  28263  fusgreghash2wspv  28372  ex-hash  28490  fsupprnfi  30700  ffsrn  30738  fsumiunle  30817  fply1  31335  locfinref  31459  esumcst  31697  esumsnf  31698  hasheuni  31719  rossros  31814  sibf0  31967  eulerpartlems  31993  eulerpartlemb  32001  ccatmulgnn0dir  32187  ofcccat  32188  plymulx0  32192  prodfzo03  32249  breprexp  32279  hgt750lemb  32302  hgt750leme  32304  lpadlem2  32326  derangsn  32799  onsucsuccmpi  34318  topdifinffinlem  35204  pibt2  35274  finixpnum  35448  lindsenlbs  35458  poimirlem26  35489  poimirlem27  35490  poimirlem31  35494  poimirlem32  35495  prdsbnd  35637  heiborlem3  35657  heiborlem8  35662  ismrer1  35682  reheibor  35683  pclfinN  37600  frlmvscadiccat  39891  frlmsnic  39916  evlsbagval  39926  mhphf  39936  elrfi  40160  mzpcompact2lem  40217  dfac11  40531  pwslnmlem0  40560  lpirlnr  40586  mpct  42355  cnrefiisplem  42988  dvmptfprodlem  43103  dvnprodlem2  43106  stoweidlem44  43203  fourierdlem51  43316  fourierdlem80  43345  fouriersw  43390  salexct  43491  salexct3  43499  salgencntex  43500  salgensscntex  43501  sge0sn  43535  sge0tsms  43536  sge0cl  43537  sge0sup  43547  sge0iunmptlemfi  43569  sge0splitsn  43597  hoiprodp1  43744  sge0hsphoire  43745  hoidmv1le  43750  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem5  43755  hspmbllem2  43783  ovnovollem3  43814  vonvolmbl  43817  vonvol  43818  vonvol2  43820  fsummmodsnunz  44443  suppmptcfin  45331  lcosn0  45377  lincext2  45412  snlindsntor  45428