Theorem snfi 9040

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 8635	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9015	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5151	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3612	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		snprc 4720	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
7		en0 9009	. . . . 5 ⊢ ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8		peano1 7875	. . . . . 6 ⊢ ∅ ∈ ω
9		breq2 5151	. . . . . . 7 ⊢ (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
10	9	rspcev 3612	. . . . . 6 ⊢ ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
11	8, 10	mpan 688	. . . . 5 ⊢ ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
12	7, 11	sylbir 234	. . . 4 ⊢ ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
13	6, 12	sylbi 216	. . 3 ⊢ (¬ 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
14	5, 13	pm2.61i 182	. 2 ⊢ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥
15		isfi 8968	. 2 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
16	14, 15	mpbir 230	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2106  ∃wrex 3070  Vcvv 3474  ∅c0 4321  {csn 4627   class class class wbr 5147  ωcom 7851  1_oc1o 8455   ≈ cen 8932  Fincfn 8935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-mo 2534  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-om 7852  df-1o 8462  df-en 8936  df-fin 8939

This theorem is referenced by:  fiprc  9041  ssfi  9169  imafi  9171  pwfi  9174  cnvfi  9176  fnfi  9177  sucdom2  9202  prfi  9318  tpfi  9319  unifpw  9351  snopfsupp  9382  sniffsupp  9391  ssfii  9410  cantnfp1lem1  9669  infpwfidom  10019  ficardadju  10190  ackbij1lem4  10214  ackbij1lem9  10219  ackbij1lem10  10220  fin23lem21  10330  isfin1-3  10377  axcclem  10448  zornn0g  10496  hashsng  14325  hashen1  14326  hashunsng  14348  hashunsngx  14349  hashprg  14351  hashsnlei  14374  hashxplem  14389  hashmap  14391  hashfun  14393  hashbclem  14407  hashf1lem1OLD  14412  hashf1lem2  14413  hashf1  14414  fsumsplitsn  15686  fsummsnunz  15696  fsumsplitsnun  15697  fsum2dlem  15712  fsumcom2  15716  ackbijnn  15770  incexclem  15778  isumltss  15790  fprod2dlem  15920  fprodcom2  15924  fprodsplitsn  15929  rexpen  16167  2ebits  16384  lcmfunsnlem2lem1  16571  lcmfunsnlem2lem2  16572  lcmfunsnlem2  16573  lcmfass  16579  phicl2  16697  ramub1lem1  16955  cshwshashnsame  17033  acsfn1  17601  acsfiindd  18502  efmnd1hash  18769  symg1hash  19251  odcau  19466  sylow2alem2  19480  gsumsnfd  19813  gsumzunsnd  19818  gsumunsnfd  19819  gsumpt  19824  ablfac1eu  19937  pgpfaclem2  19946  ablfaclem3  19951  srgbinomlem4  20045  acsfn1p  20407  uvcff  21337  psrlidm  21514  psrridm  21515  mvrcl  21542  mplsubrg  21555  mplmon  21581  mplmonmul  21582  psrbagsn  21615  psr1baslem  21700  mat1dimelbas  21964  mat1dim0  21966  mat1dimid  21967  mat1dimmul  21969  mat1dimcrng  21970  mat1f1o  21971  mat1ghm  21976  mat1mhm  21977  mat1rhm  21978  mat1scmat  22032  mvmumamul1  22047  mdetrsca  22096  mdetunilem9  22113  mdetmul  22116  pmatcoe1fsupp  22194  d1mat2pmat  22232  pmatcollpw3fi1lem1  22279  chpmat1dlem  22328  chpmat1d  22329  0cmp  22889  discmp  22893  bwth  22905  disllycmp  22993  dis1stc  22994  locfincmp  23021  dissnlocfin  23024  comppfsc  23027  1stckgenlem  23048  ptpjpre2  23075  ptopn2  23079  xkohaus  23148  xkoptsub  23149  ptcmpfi  23308  cfinufil  23423  ufinffr  23424  fin1aufil  23427  alexsubALTlem3  23544  ptcmplem5  23551  tmdgsum  23590  tsmsxplem1  23648  tsmsxplem2  23649  prdsmet  23867  imasdsf1olem  23870  prdsbl  23991  icccmplem1  24329  icccmplem2  24330  ovolsn  25003  ovolfiniun  25009  volfiniun  25055  i1f0  25195  fta1glem2  25675  fta1blem  25677  fta1lem  25811  vieta1lem2  25815  vieta1  25816  aalioulem2  25837  tayl0  25865  radcnv0  25919  wilthlem2  26562  fsumvma  26705  dchrfi  26747  cusgrfilem3  28703  eupth2eucrct  29459  trlsegvdeglem7  29468  fusgreghash2wspv  29577  ex-hash  29695  fsupprnfi  31901  ffsrn  31941  fsumiunle  32022  fply1  32625  locfinref  32809  esumcst  33049  esumsnf  33050  hasheuni  33071  rossros  33166  sibf0  33321  eulerpartlems  33347  eulerpartlemb  33355  ccatmulgnn0dir  33541  ofcccat  33542  plymulx0  33546  prodfzo03  33603  breprexp  33633  hgt750lemb  33656  hgt750leme  33658  lpadlem2  33680  derangsn  34149  onsucsuccmpi  35316  topdifinffinlem  36216  pibt2  36286  finixpnum  36461  lindsenlbs  36471  poimirlem26  36502  poimirlem27  36503  poimirlem31  36507  poimirlem32  36508  prdsbnd  36649  heiborlem3  36669  heiborlem8  36674  ismrer1  36694  reheibor  36695  pclfinN  38759  frlmvscadiccat  41077  frlmsnic  41107  selvvvval  41154  elrfi  41417  mzpcompact2lem  41474  dfac11  41789  pwslnmlem0  41818  lpirlnr  41844  mpct  43885  cnrefiisplem  44531  dvmptfprodlem  44646  dvnprodlem2  44649  stoweidlem44  44746  fourierdlem51  44859  fourierdlem80  44888  fouriersw  44933  salexct  45036  salexct3  45044  salgencntex  45045  salgensscntex  45046  sge0sn  45081  sge0tsms  45082  sge0cl  45083  sge0sup  45093  sge0iunmptlemfi  45115  sge0splitsn  45143  hoiprodp1  45290  sge0hsphoire  45291  hoidmv1le  45296  hoidmvlelem1  45297  hoidmvlelem2  45298  hoidmvlelem5  45301  hspmbllem2  45329  ovnovollem3  45360  vonvolmbl  45363  vonvol  45364  vonvol2  45366  fsummmodsnunz  46029  suppmptcfin  47008  lcosn0  47054  lincext2  47089  snlindsntor  47105