Theorem snfi 8588

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 8259	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8568	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5062	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3622	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 589	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		snprc 4646	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
7		en0 8566	. . . . 5 ⊢ ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8		peano1 7595	. . . . . 6 ⊢ ∅ ∈ ω
9		breq2 5062	. . . . . . 7 ⊢ (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
10	9	rspcev 3622	. . . . . 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 8527	. 2 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
16	14, 15	mpbir 233	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1533   ∈ wcel 2110  ∃wrex 3139  Vcvv 3494  ∅c0 4290  {csn 4560   class class class wbr 5058  ωcom 7574  1_oc1o 8089   ≈ cen 8500  Fincfn 8503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  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 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-om 7575  df-1o 8096  df-en 8504  df-fin 8507

This theorem is referenced by:  fiprc  8589  prfi  8787  tpfi  8788  fnfi  8790  unifpw  8821  snopfsupp  8850  sniffsupp  8867  ssfii  8877  cantnfp1lem1  9135  infpwfidom  9448  ackbij1lem4  9639  ackbij1lem9  9644  ackbij1lem10  9645  fin23lem21  9755  isfin1-3  9802  axcclem  9873  zornn0g  9921  hashsng  13724  hashen1  13725  hashunsng  13747  hashunsngx  13748  hashprg  13750  hashsnlei  13773  hashxplem  13788  hashmap  13790  hashfun  13792  hashbclem  13804  hashf1lem1  13807  hashf1lem2  13808  hashf1  13809  fsumsplitsn  15094  fsummsnunz  15103  fsumsplitsnun  15104  fsum2dlem  15119  fsumcom2  15123  ackbijnn  15177  incexclem  15185  isumltss  15197  fprod2dlem  15328  fprodcom2  15332  fprodsplitsn  15337  rexpen  15575  2ebits  15790  lcmfunsnlem2lem1  15976  lcmfunsnlem2lem2  15977  lcmfunsnlem2  15978  lcmfass  15984  phicl2  16099  ramub1lem1  16356  cshwshashnsame  16431  acsfn1  16926  acsfiindd  17781  efmnd1hash  18051  symg1hash  18512  odcau  18723  sylow2alem2  18737  gsumsnfd  19065  gsumzunsnd  19070  gsumunsnfd  19071  gsumpt  19076  ablfac1eu  19189  pgpfaclem2  19198  ablfaclem3  19203  srgbinomlem4  19287  acsfn1p  19572  psrlidm  20177  psrridm  20178  mplsubrg  20214  mvrcl  20223  mplmon  20238  mplmonmul  20239  psrbagsn  20269  psr1baslem  20347  uvcff  20929  mat1dimelbas  21074  mat1dim0  21076  mat1dimid  21077  mat1dimmul  21079  mat1dimcrng  21080  mat1f1o  21081  mat1ghm  21086  mat1mhm  21087  mat1rhm  21088  mat1rngiso  21089  mat1scmat  21142  mvmumamul1  21157  mdetrsca  21206  mdetunilem9  21223  mdetmul  21226  pmatcoe1fsupp  21303  d1mat2pmat  21341  pmatcollpw3fi1lem1  21388  chpmat1dlem  21437  chpmat1d  21438  0cmp  21996  discmp  22000  bwth  22012  disllycmp  22100  dis1stc  22101  locfincmp  22128  dissnlocfin  22131  comppfsc  22134  1stckgenlem  22155  ptpjpre2  22182  ptopn2  22186  xkohaus  22255  xkoptsub  22256  ptcmpfi  22415  cfinufil  22530  ufinffr  22531  fin1aufil  22534  alexsubALTlem3  22651  ptcmplem5  22658  tmdgsum  22697  tsmsxplem1  22755  tsmsxplem2  22756  prdsmet  22974  imasdsf1olem  22977  prdsbl  23095  icccmplem1  23424  icccmplem2  23425  ovolsn  24090  ovolfiniun  24096  volfiniun  24142  i1f0  24282  fta1glem2  24754  fta1blem  24756  fta1lem  24890  vieta1lem2  24894  vieta1  24895  aalioulem2  24916  tayl0  24944  radcnv0  24998  wilthlem2  25640  fsumvma  25783  dchrfi  25825  cusgrfilem3  27233  eupth2eucrct  27990  trlsegvdeglem7  27999  fusgreghash2wspv  28108  ex-hash  28226  ffsrn  30459  fsumiunle  30540  fply1  30926  locfinref  31100  esumcst  31317  esumsnf  31318  hasheuni  31339  rossros  31434  sibf0  31587  eulerpartlems  31613  eulerpartlemb  31621  ccatmulgnn0dir  31807  ofcccat  31808  plymulx0  31812  prodfzo03  31869  breprexp  31899  hgt750lemb  31922  hgt750leme  31924  lpadlem2  31946  derangsn  32412  onsucsuccmpi  33786  topdifinffinlem  34622  pibt2  34692  finixpnum  34871  lindsenlbs  34881  poimirlem26  34912  poimirlem27  34913  poimirlem31  34917  poimirlem32  34918  prdsbnd  35065  heiborlem3  35085  heiborlem8  35090  ismrer1  35110  reheibor  35111  pclfinN  37030  frlmvscadiccat  39138  frlmsnic  39142  elrfi  39284  mzpcompact2lem  39341  dfac11  39655  pwslnmlem0  39684  lpirlnr  39710  mpct  41457  cnrefiisplem  42103  dvmptfprodlem  42222  dvnprodlem2  42225  stoweidlem44  42323  fourierdlem51  42436  fourierdlem80  42465  fouriersw  42510  salexct  42611  salexct3  42619  salgencntex  42620  salgensscntex  42621  sge0sn  42655  sge0tsms  42656  sge0cl  42657  sge0sup  42667  sge0iunmptlemfi  42689  sge0splitsn  42717  hoiprodp1  42864  sge0hsphoire  42865  hoidmv1le  42870  hoidmvlelem1  42871  hoidmvlelem2  42872  hoidmvlelem5  42875  hspmbllem2  42903  ovnovollem3  42934  vonvolmbl  42937  vonvol  42938  vonvol2  42940  fsummmodsnunz  43529  suppmptcfin  44421  lcosn0  44469  lincext2  44504  snlindsntor  44520