Theorem snfi 8594

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 8265	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8574	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5070	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3623	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 589	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		snprc 4653	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
7		en0 8572	. . . . 5 ⊢ ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8		peano1 7601	. . . . . 6 ⊢ ∅ ∈ ω
9		breq2 5070	. . . . . . 7 ⊢ (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
10	9	rspcev 3623	. . . . . 6 ⊢ ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
11	8, 10	mpan 688	. . . . 5 ⊢ ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
12	7, 11	sylbir 237	. . . 4 ⊢ ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
13	6, 12	sylbi 219	. . 3 ⊢ (¬ 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
14	5, 13	pm2.61i 184	. 2 ⊢ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥
15		isfi 8533	. 2 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
16	14, 15	mpbir 233	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1537   ∈ wcel 2114  ∃wrex 3139  Vcvv 3494  ∅c0 4291  {csn 4567   class class class wbr 5066  ωcom 7580  1_oc1o 8095   ≈ cen 8506  Fincfn 8509

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-om 7581  df-1o 8102  df-en 8510  df-fin 8513

This theorem is referenced by:  fiprc  8595  prfi  8793  tpfi  8794  fnfi  8796  unifpw  8827  snopfsupp  8856  sniffsupp  8873  ssfii  8883  cantnfp1lem1  9141  infpwfidom  9454  ackbij1lem4  9645  ackbij1lem9  9650  ackbij1lem10  9651  fin23lem21  9761  isfin1-3  9808  axcclem  9879  zornn0g  9927  hashsng  13731  hashen1  13732  hashunsng  13754  hashunsngx  13755  hashprg  13757  hashsnlei  13780  hashxplem  13795  hashmap  13797  hashfun  13799  hashbclem  13811  hashf1lem1  13814  hashf1lem2  13815  hashf1  13816  fsumsplitsn  15100  fsummsnunz  15109  fsumsplitsnun  15110  fsum2dlem  15125  fsumcom2  15129  ackbijnn  15183  incexclem  15191  isumltss  15203  fprod2dlem  15334  fprodcom2  15338  fprodsplitsn  15343  rexpen  15581  2ebits  15796  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  lcmfass  15990  phicl2  16105  ramub1lem1  16362  cshwshashnsame  16437  acsfn1  16932  acsfiindd  17787  efmnd1hash  18057  symg1hash  18518  odcau  18729  sylow2alem2  18743  gsumsnfd  19071  gsumzunsnd  19076  gsumunsnfd  19077  gsumpt  19082  ablfac1eu  19195  pgpfaclem2  19204  ablfaclem3  19209  srgbinomlem4  19293  acsfn1p  19578  psrlidm  20183  psrridm  20184  mplsubrg  20220  mvrcl  20229  mplmon  20244  mplmonmul  20245  psrbagsn  20275  psr1baslem  20353  uvcff  20935  mat1dimelbas  21080  mat1dim0  21082  mat1dimid  21083  mat1dimmul  21085  mat1dimcrng  21086  mat1f1o  21087  mat1ghm  21092  mat1mhm  21093  mat1rhm  21094  mat1rngiso  21095  mat1scmat  21148  mvmumamul1  21163  mdetrsca  21212  mdetunilem9  21229  mdetmul  21232  pmatcoe1fsupp  21309  d1mat2pmat  21347  pmatcollpw3fi1lem1  21394  chpmat1dlem  21443  chpmat1d  21444  0cmp  22002  discmp  22006  bwth  22018  disllycmp  22106  dis1stc  22107  locfincmp  22134  dissnlocfin  22137  comppfsc  22140  1stckgenlem  22161  ptpjpre2  22188  ptopn2  22192  xkohaus  22261  xkoptsub  22262  ptcmpfi  22421  cfinufil  22536  ufinffr  22537  fin1aufil  22540  alexsubALTlem3  22657  ptcmplem5  22664  tmdgsum  22703  tsmsxplem1  22761  tsmsxplem2  22762  prdsmet  22980  imasdsf1olem  22983  prdsbl  23101  icccmplem1  23430  icccmplem2  23431  ovolsn  24096  ovolfiniun  24102  volfiniun  24148  i1f0  24288  fta1glem2  24760  fta1blem  24762  fta1lem  24896  vieta1lem2  24900  vieta1  24901  aalioulem2  24922  tayl0  24950  radcnv0  25004  wilthlem2  25646  fsumvma  25789  dchrfi  25831  cusgrfilem3  27239  eupth2eucrct  27996  trlsegvdeglem7  28005  fusgreghash2wspv  28114  ex-hash  28232  ffsrn  30465  fsumiunle  30545  fply1  30931  locfinref  31105  esumcst  31322  esumsnf  31323  hasheuni  31344  rossros  31439  sibf0  31592  eulerpartlems  31618  eulerpartlemb  31626  ccatmulgnn0dir  31812  ofcccat  31813  plymulx0  31817  prodfzo03  31874  breprexp  31904  hgt750lemb  31927  hgt750leme  31929  lpadlem2  31951  derangsn  32417  onsucsuccmpi  33791  topdifinffinlem  34631  pibt2  34701  finixpnum  34892  lindsenlbs  34902  poimirlem26  34933  poimirlem27  34934  poimirlem31  34938  poimirlem32  34939  prdsbnd  35086  heiborlem3  35106  heiborlem8  35111  ismrer1  35131  reheibor  35132  pclfinN  37051  frlmvscadiccat  39165  frlmsnic  39169  elrfi  39311  mzpcompact2lem  39368  dfac11  39682  pwslnmlem0  39711  lpirlnr  39737  mpct  41484  cnrefiisplem  42130  dvmptfprodlem  42249  dvnprodlem2  42252  stoweidlem44  42349  fourierdlem51  42462  fourierdlem80  42491  fouriersw  42536  salexct  42637  salexct3  42645  salgencntex  42646  salgensscntex  42647  sge0sn  42681  sge0tsms  42682  sge0cl  42683  sge0sup  42693  sge0iunmptlemfi  42715  sge0splitsn  42743  hoiprodp1  42890  sge0hsphoire  42891  hoidmv1le  42896  hoidmvlelem1  42897  hoidmvlelem2  42898  hoidmvlelem5  42901  hspmbllem2  42929  ovnovollem3  42960  vonvolmbl  42963  vonvol  42964  vonvol2  42966  fsummmodsnunz  43555  suppmptcfin  44447  lcosn0  44495  lincext2  44530  snlindsntor  44546