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

Theorem ssfi 8333
Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. (Contributed by NM, 24-Jun-1998.)
Assertion
Ref Expression
ssfi ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin)

Proof of Theorem ssfi
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 8133 . . 3 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
2 bren 8118 . . . . 5 (𝐴𝑥 ↔ ∃𝑧 𝑧:𝐴1-1-onto𝑥)
3 f1ofo 6293 . . . . . . . . . . 11 (𝑧:𝐴1-1-onto𝑥𝑧:𝐴onto𝑥)
4 imassrn 5623 . . . . . . . . . . . 12 (𝑧𝐵) ⊆ ran 𝑧
5 forn 6267 . . . . . . . . . . . 12 (𝑧:𝐴onto𝑥 → ran 𝑧 = 𝑥)
64, 5syl5sseq 3782 . . . . . . . . . . 11 (𝑧:𝐴onto𝑥 → (𝑧𝐵) ⊆ 𝑥)
73, 6syl 17 . . . . . . . . . 10 (𝑧:𝐴1-1-onto𝑥 → (𝑧𝐵) ⊆ 𝑥)
8 ssnnfi 8332 . . . . . . . . . . 11 ((𝑥 ∈ ω ∧ (𝑧𝐵) ⊆ 𝑥) → (𝑧𝐵) ∈ Fin)
9 isfi 8133 . . . . . . . . . . 11 ((𝑧𝐵) ∈ Fin ↔ ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
108, 9sylib 208 . . . . . . . . . 10 ((𝑥 ∈ ω ∧ (𝑧𝐵) ⊆ 𝑥) → ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
117, 10sylan2 492 . . . . . . . . 9 ((𝑥 ∈ ω ∧ 𝑧:𝐴1-1-onto𝑥) → ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
1211adantrr 755 . . . . . . . 8 ((𝑥 ∈ ω ∧ (𝑧:𝐴1-1-onto𝑥𝐵𝐴)) → ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
13 f1of1 6285 . . . . . . . . . . . . . 14 (𝑧:𝐴1-1-onto𝑥𝑧:𝐴1-1𝑥)
14 f1ores 6300 . . . . . . . . . . . . . 14 ((𝑧:𝐴1-1𝑥𝐵𝐴) → (𝑧𝐵):𝐵1-1-onto→(𝑧𝐵))
1513, 14sylan 489 . . . . . . . . . . . . 13 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → (𝑧𝐵):𝐵1-1-onto→(𝑧𝐵))
16 vex 3331 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
1716resex 5589 . . . . . . . . . . . . . . . 16 (𝑧𝐵) ∈ V
18 f1oeq1 6276 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑧𝐵) → (𝑥:𝐵1-1-onto→(𝑧𝐵) ↔ (𝑧𝐵):𝐵1-1-onto→(𝑧𝐵)))
1917, 18spcev 3428 . . . . . . . . . . . . . . 15 ((𝑧𝐵):𝐵1-1-onto→(𝑧𝐵) → ∃𝑥 𝑥:𝐵1-1-onto→(𝑧𝐵))
20 bren 8118 . . . . . . . . . . . . . . 15 (𝐵 ≈ (𝑧𝐵) ↔ ∃𝑥 𝑥:𝐵1-1-onto→(𝑧𝐵))
2119, 20sylibr 224 . . . . . . . . . . . . . 14 ((𝑧𝐵):𝐵1-1-onto→(𝑧𝐵) → 𝐵 ≈ (𝑧𝐵))
22 entr 8161 . . . . . . . . . . . . . 14 ((𝐵 ≈ (𝑧𝐵) ∧ (𝑧𝐵) ≈ 𝑦) → 𝐵𝑦)
2321, 22sylan 489 . . . . . . . . . . . . 13 (((𝑧𝐵):𝐵1-1-onto→(𝑧𝐵) ∧ (𝑧𝐵) ≈ 𝑦) → 𝐵𝑦)
2415, 23sylan 489 . . . . . . . . . . . 12 (((𝑧:𝐴1-1-onto𝑥𝐵𝐴) ∧ (𝑧𝐵) ≈ 𝑦) → 𝐵𝑦)
2524ex 449 . . . . . . . . . . 11 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → ((𝑧𝐵) ≈ 𝑦𝐵𝑦))
2625reximdv 3142 . . . . . . . . . 10 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → (∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦 → ∃𝑦 ∈ ω 𝐵𝑦))
27 isfi 8133 . . . . . . . . . 10 (𝐵 ∈ Fin ↔ ∃𝑦 ∈ ω 𝐵𝑦)
2826, 27syl6ibr 242 . . . . . . . . 9 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → (∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦𝐵 ∈ Fin))
2928adantl 473 . . . . . . . 8 ((𝑥 ∈ ω ∧ (𝑧:𝐴1-1-onto𝑥𝐵𝐴)) → (∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦𝐵 ∈ Fin))
3012, 29mpd 15 . . . . . . 7 ((𝑥 ∈ ω ∧ (𝑧:𝐴1-1-onto𝑥𝐵𝐴)) → 𝐵 ∈ Fin)
3130exp32 632 . . . . . 6 (𝑥 ∈ ω → (𝑧:𝐴1-1-onto𝑥 → (𝐵𝐴𝐵 ∈ Fin)))
3231exlimdv 1998 . . . . 5 (𝑥 ∈ ω → (∃𝑧 𝑧:𝐴1-1-onto𝑥 → (𝐵𝐴𝐵 ∈ Fin)))
332, 32syl5bi 232 . . . 4 (𝑥 ∈ ω → (𝐴𝑥 → (𝐵𝐴𝐵 ∈ Fin)))
3433rexlimiv 3153 . . 3 (∃𝑥 ∈ ω 𝐴𝑥 → (𝐵𝐴𝐵 ∈ Fin))
351, 34sylbi 207 . 2 (𝐴 ∈ Fin → (𝐵𝐴𝐵 ∈ Fin))
3635imp 444 1 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wex 1841  wcel 2127  wrex 3039  wss 3703   class class class wbr 4792  ran crn 5255  cres 5256  cima 5257  1-1wf1 6034  ontowfo 6035  1-1-ontowf1o 6036  ωcom 7218  cen 8106  Fincfn 8109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-om 7219  df-er 7899  df-en 8110  df-fin 8113
This theorem is referenced by:  domfi  8334  ssfid  8336  infi  8337  finresfin  8339  diffi  8345  findcard3  8356  unfir  8381  fnfi  8391  fofinf1o  8394  cnvfi  8401  f1fi  8406  imafi  8412  mapfi  8415  ixpfi  8416  ixpfi2  8417  mptfi  8418  cnvimamptfin  8420  fisuppfi  8436  suppssfifsupp  8443  fsuppunbi  8449  snopfsupp  8451  fsuppres  8453  ressuppfi  8454  fsuppmptif  8458  fsuppco2  8461  fsuppcor  8462  sniffsupp  8468  elfiun  8489  wemapso2lem  8610  cantnfp1lem1  8736  oemapvali  8742  ackbij2lem1  9204  ackbij1lem11  9215  fin23lem26  9310  fin23lem23  9311  fin23lem21  9324  fin11a  9368  isfin1-3  9371  axcclem  9442  ssnn0fi  12949  hashun3  13336  hashss  13360  hashssdif  13363  hashsslei  13376  hashreshashfun  13389  hashbclem  13399  hashf1lem2  13403  seqcoll2  13412  pr2pwpr  13424  isercolllem2  14566  isercoll  14568  fsum2dlem  14671  fsumcom2OLD  14676  fsumless  14698  fsumabs  14703  fsumrlim  14713  fsumo1  14714  cvgcmpce  14720  fsumiun  14723  qshash  14729  incexclem  14738  incexc  14739  incexc2  14740  fprod2dlem  14880  fprodcom2OLD  14885  fprodmodd  14898  sumeven  15283  sumodd  15284  bitsfi  15332  bitsinv1  15337  bitsinvp1  15344  sadcaddlem  15352  sadadd2lem  15354  sadadd3  15356  sadaddlem  15361  sadasslem  15365  sadeq  15367  phicl2  15646  phibnd  15649  hashdvds  15653  phiprmpw  15654  phimullem  15657  eulerthlem2  15660  eulerth  15661  phisum  15668  sumhash  15773  prmreclem2  15794  prmreclem3  15795  prmreclem4  15796  prmreclem5  15797  1arith  15804  4sqlem11  15832  vdwlem11  15868  hashbccl  15880  ramlb  15896  0ram  15897  ramub1lem1  15903  ramub1lem2  15904  prmgaplem3  15930  prmgaplem4  15931  isstruct2  16040  lagsubg2  17827  lagsubg  17828  orbsta2  17918  symgbasfi  17977  symgfisg  18059  symggen2  18062  odcl2  18153  oddvds2  18154  sylow1lem2  18185  sylow1lem3  18186  sylow1lem4  18187  sylow1lem5  18188  odcau  18190  pgpssslw  18200  sylow2alem2  18204  sylow2a  18205  sylow2blem1  18206  sylow2blem3  18208  slwhash  18210  fislw  18211  sylow2  18212  sylow3lem1  18213  sylow3lem3  18215  sylow3lem4  18216  sylow3lem6  18218  cyggenod  18457  gsumval3lem1  18477  gsumval3lem2  18478  gsumval3  18479  gsumzadd  18493  gsumpt  18532  gsum2dlem1  18540  gsum2dlem2  18541  gsum2d  18542  gsum2d2lem  18543  dprdfadd  18590  ablfacrplem  18635  ablfacrp2  18637  ablfac1c  18641  ablfac1eulem  18642  ablfac1eu  18643  pgpfac1lem5  18649  pgpfaclem2  18652  pgpfaclem3  18653  ablfaclem3  18657  lcomfsupp  19076  psrbaglecl  19542  psrbagaddcl  19543  psrbagcon  19544  mplsubg  19610  mpllss  19611  mplcoe5  19641  psrbagsn  19668  psr1baslem  19728  dsmmfi  20255  dsmmacl  20258  dsmmsubg  20260  dsmmlss  20261  frlmsslsp  20308  mamures  20369  submabas  20557  mdetdiaglem  20577  mdetrlin  20581  mdetrsca  20582  mdetralt  20587  maducoeval2  20619  madugsum  20622  fctop  20981  restfpw  21156  fincmp  21369  cmpfi  21384  bwth  21386  finlocfin  21496  lfinpfin  21500  locfincmp  21502  1stckgenlem  21529  ptbasfi  21557  ptcnplem  21597  ptcmpfi  21789  cfinfil  21869  ufinffr  21905  fin1aufil  21908  tsmsres  22119  xrge0gsumle  22808  xrge0tsms  22809  fsumcn  22845  rrxcph  23351  rrxmval  23359  ovoliunlem1  23441  ovolicc2lem4  23459  ovolicc2lem5  23460  i1fima  23615  i1fd  23618  itg1cl  23622  itg1ge0  23623  i1f0  23624  i1f1  23627  i1fadd  23632  i1fmul  23633  itg1addlem4  23636  i1fmulc  23640  itg1mulc  23641  i1fres  23642  itg10a  23647  itg1ge0a  23648  itg1climres  23651  mbfi1fseqlem4  23655  itgfsum  23763  dvmptfsum  23908  plyexmo  24238  aannenlem2  24254  aalioulem2  24258  birthday  24851  jensenlem1  24883  jensenlem2  24884  jensen  24885  wilthlem2  24965  ppifi  25002  prmdvdsfi  25003  0sgm  25040  sgmf  25041  sgmnncl  25043  ppiprm  25047  chtprm  25049  chtdif  25054  efchtdvds  25055  ppidif  25059  ppiltx  25073  mumul  25077  sqff1o  25078  fsumdvdsdiag  25080  fsumdvdscom  25081  dvdsflsumcom  25084  musum  25087  musumsum  25088  muinv  25089  fsumdvdsmul  25091  ppiub  25099  vmasum  25111  logfac2  25112  perfectlem2  25125  dchrfi  25150  dchrabs  25155  dchrptlem1  25159  dchrptlem2  25160  dchrpt  25162  lgsquadlem1  25275  lgsquadlem2  25276  lgsquadlem3  25277  chebbnd1lem1  25328  chtppilimlem1  25332  rplogsumlem2  25344  rpvmasumlem  25346  dchrvmasumlem1  25354  dchrisum0ff  25366  rpvmasum2  25371  dchrisum0re  25372  dchrisum0  25379  rplogsum  25386  dirith2  25387  vmalogdivsum2  25397  logsqvma  25401  logsqvma2  25402  selberg  25407  selberg34r  25430  pntsval2  25435  pntrlog2bndlem1  25436  cusgrfi  26535  wwlksnfi  26995  hashwwlksnext  27003  relfi  29693  imafi2  29769  unifi3  29770  ffsrn  29784  gsumle  30059  xrge0tsmsd  30065  hasheuni  30427  carsgclctunlem1  30659  sibfof  30682  sitgclg  30684  oddpwdc  30696  eulerpartlems  30702  eulerpartlemb  30710  eulerpartlemmf  30717  eulerpartlemgf  30721  eulerpartlemgs2  30722  coinfliplem  30820  coinflippv  30825  ballotlemfelz  30832  ballotlemfp1  30833  ballotlemfc0  30834  ballotlemfcc  30835  ballotlemiex  30843  ballotlemsup  30846  ballotlemfg  30867  ballotlemfrc  30868  ballotlemfrceq  30870  ballotth  30879  breprexpnat  30992  hgt750lemb  31014  hgt750leme  31016  deranglem  31426  subfacp1lem3  31442  subfacp1lem5  31444  subfacp1lem6  31445  erdszelem2  31452  erdszelem8  31458  erdsze2lem2  31464  snmlff  31589  mvrsfpw  31681  finminlem  32589  topdifinffinlem  33477  matunitlindflem1  33687  poimirlem9  33700  poimirlem26  33717  poimirlem27  33718  poimirlem28  33719  poimirlem30  33721  poimirlem32  33723  itg2addnclem2  33744  nnubfi  33828  nninfnub  33829  sstotbnd2  33855  cntotbnd  33877  rencldnfilem  37855  jm2.22  38033  jm2.23  38034  filnm  38131  pwssfi  39679  disjinfi  39848  fsumiunss  40279  fprodexp  40298  fprodabs2  40299  mccllem  40301  sumnnodd  40334  fprodcncf  40586  dvmptfprod  40632  dvnprodlem1  40633  dvnprodlem2  40634  fourierdlem25  40821  fourierdlem37  40833  fourierdlem51  40846  fourierdlem79  40874  fouriersw  40920  etransclem16  40939  etransclem24  40947  etransclem33  40956  etransclem44  40967  sge0resplit  41095  sge0iunmptlemfi  41102  sge0iunmptlemre  41104  carageniuncllem2  41211  hsphoidmvle2  41274  hsphoidmvle  41275  hoidmvlelem4  41287  hoidmvlelem5  41288  fmtnoinf  41927  perfectALTVlem2  42110  rmsuppfi  42633  mndpsuppfi  42635  scmsuppfi  42637  suppmptcfin  42639
  Copyright terms: Public domain W3C validator