MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snfi Structured version   Visualization version   GIF version

Theorem snfi 8581
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.
StepHypRef Expression
1 1onn 8252 . . . 4 1o ∈ ω
2 ensn1g 8561 . . . 4 (𝐴 ∈ V → {𝐴} ≈ 1o)
3 breq2 5037 . . . . 5 (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
43rspcev 3574 . . . 4 ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
51, 2, 4sylancr 590 . . 3 (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6 snprc 4616 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
7 en0 8559 . . . . 5 ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8 peano1 7585 . . . . . 6 ∅ ∈ ω
9 breq2 5037 . . . . . . 7 (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
109rspcev 3574 . . . . . 6 ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
118, 10mpan 689 . . . . 5 ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
127, 11sylbir 238 . . . 4 ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
136, 12sylbi 220 . . 3 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
145, 13pm2.61i 185 . 2 𝑥 ∈ ω {𝐴} ≈ 𝑥
15 isfi 8520 . 2 ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
1614, 15mpbir 234 1 {𝐴} ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1538  wcel 2112  wrex 3110  Vcvv 3444  c0 4246  {csn 4528   class class class wbr 5033  ωcom 7564  1oc1o 8082  cen 8493  Fincfn 8496
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-om 7565  df-1o 8089  df-en 8497  df-fin 8500
This theorem is referenced by:  fiprc  8582  prfi  8781  tpfi  8782  fnfi  8784  unifpw  8815  snopfsupp  8844  sniffsupp  8861  ssfii  8871  cantnfp1lem1  9129  infpwfidom  9443  ficardadju  9614  ackbij1lem4  9638  ackbij1lem9  9643  ackbij1lem10  9644  fin23lem21  9754  isfin1-3  9801  axcclem  9872  zornn0g  9920  hashsng  13730  hashen1  13731  hashunsng  13753  hashunsngx  13754  hashprg  13756  hashsnlei  13779  hashxplem  13794  hashmap  13796  hashfun  13798  hashbclem  13810  hashf1lem1  13813  hashf1lem2  13814  hashf1  13815  fsumsplitsn  15095  fsummsnunz  15104  fsumsplitsnun  15105  fsum2dlem  15120  fsumcom2  15124  ackbijnn  15178  incexclem  15186  isumltss  15198  fprod2dlem  15329  fprodcom2  15333  fprodsplitsn  15338  rexpen  15576  2ebits  15789  lcmfunsnlem2lem1  15975  lcmfunsnlem2lem2  15976  lcmfunsnlem2  15977  lcmfass  15983  phicl2  16098  ramub1lem1  16355  cshwshashnsame  16432  acsfn1  16927  acsfiindd  17782  efmnd1hash  18052  symg1hash  18513  odcau  18724  sylow2alem2  18738  gsumsnfd  19067  gsumzunsnd  19072  gsumunsnfd  19073  gsumpt  19078  ablfac1eu  19191  pgpfaclem2  19200  ablfaclem3  19205  srgbinomlem4  19289  acsfn1p  19574  uvcff  20483  psrlidm  20644  psrridm  20645  mplsubrg  20681  mvrcl  20691  mplmon  20706  mplmonmul  20707  psrbagsn  20737  psr1baslem  20817  mat1dimelbas  21079  mat1dim0  21081  mat1dimid  21082  mat1dimmul  21084  mat1dimcrng  21085  mat1f1o  21086  mat1ghm  21091  mat1mhm  21092  mat1rhm  21093  mat1rngiso  21094  mat1scmat  21147  mvmumamul1  21162  mdetrsca  21211  mdetunilem9  21228  mdetmul  21231  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  24102  ovolfiniun  24108  volfiniun  24154  i1f0  24294  fta1glem2  24770  fta1blem  24772  fta1lem  24906  vieta1lem2  24910  vieta1  24911  aalioulem2  24932  tayl0  24960  radcnv0  25014  wilthlem2  25657  fsumvma  25800  dchrfi  25842  cusgrfilem3  27250  eupth2eucrct  28005  trlsegvdeglem7  28014  fusgreghash2wspv  28123  ex-hash  28241  fsupprnfi  30455  ffsrn  30494  fsumiunle  30574  fply1  30985  locfinref  31194  esumcst  31430  esumsnf  31431  hasheuni  31452  rossros  31547  sibf0  31700  eulerpartlems  31726  eulerpartlemb  31734  ccatmulgnn0dir  31920  ofcccat  31921  plymulx0  31925  prodfzo03  31982  breprexp  32012  hgt750lemb  32035  hgt750leme  32037  lpadlem2  32059  derangsn  32525  onsucsuccmpi  33899  topdifinffinlem  34759  pibt2  34829  finixpnum  35035  lindsenlbs  35045  poimirlem26  35076  poimirlem27  35077  poimirlem31  35081  poimirlem32  35082  prdsbnd  35224  heiborlem3  35244  heiborlem8  35249  ismrer1  35269  reheibor  35270  pclfinN  37189  frlmvscadiccat  39427  frlmsnic  39440  elrfi  39622  mzpcompact2lem  39679  dfac11  39993  pwslnmlem0  40022  lpirlnr  40048  mpct  41817  cnrefiisplem  42458  dvmptfprodlem  42573  dvnprodlem2  42576  stoweidlem44  42673  fourierdlem51  42786  fourierdlem80  42815  fouriersw  42860  salexct  42961  salexct3  42969  salgencntex  42970  salgensscntex  42971  sge0sn  43005  sge0tsms  43006  sge0cl  43007  sge0sup  43017  sge0iunmptlemfi  43039  sge0splitsn  43067  hoiprodp1  43214  sge0hsphoire  43215  hoidmv1le  43220  hoidmvlelem1  43221  hoidmvlelem2  43222  hoidmvlelem5  43225  hspmbllem2  43253  ovnovollem3  43284  vonvolmbl  43287  vonvol  43288  vonvol2  43290  fsummmodsnunz  43879  suppmptcfin  44768  lcosn0  44816  lincext2  44851  snlindsntor  44867
  Copyright terms: Public domain W3C validator