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

Theorem ssfi 8221
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 8021 . . 3 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
2 bren 8006 . . . . 5 (𝐴𝑥 ↔ ∃𝑧 𝑧:𝐴1-1-onto𝑥)
3 f1ofo 6182 . . . . . . . . . . 11 (𝑧:𝐴1-1-onto𝑥𝑧:𝐴onto𝑥)
4 imassrn 5512 . . . . . . . . . . . 12 (𝑧𝐵) ⊆ ran 𝑧
5 forn 6156 . . . . . . . . . . . 12 (𝑧:𝐴onto𝑥 → ran 𝑧 = 𝑥)
64, 5syl5sseq 3686 . . . . . . . . . . 11 (𝑧:𝐴onto𝑥 → (𝑧𝐵) ⊆ 𝑥)
73, 6syl 17 . . . . . . . . . 10 (𝑧:𝐴1-1-onto𝑥 → (𝑧𝐵) ⊆ 𝑥)
8 ssnnfi 8220 . . . . . . . . . . 11 ((𝑥 ∈ ω ∧ (𝑧𝐵) ⊆ 𝑥) → (𝑧𝐵) ∈ Fin)
9 isfi 8021 . . . . . . . . . . 11 ((𝑧𝐵) ∈ Fin ↔ ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
108, 9sylib 208 . . . . . . . . . 10 ((𝑥 ∈ ω ∧ (𝑧𝐵) ⊆ 𝑥) → ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
117, 10sylan2 490 . . . . . . . . 9 ((𝑥 ∈ ω ∧ 𝑧:𝐴1-1-onto𝑥) → ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
1211adantrr 753 . . . . . . . 8 ((𝑥 ∈ ω ∧ (𝑧:𝐴1-1-onto𝑥𝐵𝐴)) → ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
13 f1of1 6174 . . . . . . . . . . . . . 14 (𝑧:𝐴1-1-onto𝑥𝑧:𝐴1-1𝑥)
14 f1ores 6189 . . . . . . . . . . . . . 14 ((𝑧:𝐴1-1𝑥𝐵𝐴) → (𝑧𝐵):𝐵1-1-onto→(𝑧𝐵))
1513, 14sylan 487 . . . . . . . . . . . . 13 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → (𝑧𝐵):𝐵1-1-onto→(𝑧𝐵))
16 vex 3234 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
1716resex 5478 . . . . . . . . . . . . . . . 16 (𝑧𝐵) ∈ V
18 f1oeq1 6165 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑧𝐵) → (𝑥:𝐵1-1-onto→(𝑧𝐵) ↔ (𝑧𝐵):𝐵1-1-onto→(𝑧𝐵)))
1917, 18spcev 3331 . . . . . . . . . . . . . . 15 ((𝑧𝐵):𝐵1-1-onto→(𝑧𝐵) → ∃𝑥 𝑥:𝐵1-1-onto→(𝑧𝐵))
20 bren 8006 . . . . . . . . . . . . . . 15 (𝐵 ≈ (𝑧𝐵) ↔ ∃𝑥 𝑥:𝐵1-1-onto→(𝑧𝐵))
2119, 20sylibr 224 . . . . . . . . . . . . . 14 ((𝑧𝐵):𝐵1-1-onto→(𝑧𝐵) → 𝐵 ≈ (𝑧𝐵))
22 entr 8049 . . . . . . . . . . . . . 14 ((𝐵 ≈ (𝑧𝐵) ∧ (𝑧𝐵) ≈ 𝑦) → 𝐵𝑦)
2321, 22sylan 487 . . . . . . . . . . . . 13 (((𝑧𝐵):𝐵1-1-onto→(𝑧𝐵) ∧ (𝑧𝐵) ≈ 𝑦) → 𝐵𝑦)
2415, 23sylan 487 . . . . . . . . . . . 12 (((𝑧:𝐴1-1-onto𝑥𝐵𝐴) ∧ (𝑧𝐵) ≈ 𝑦) → 𝐵𝑦)
2524ex 449 . . . . . . . . . . 11 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → ((𝑧𝐵) ≈ 𝑦𝐵𝑦))
2625reximdv 3045 . . . . . . . . . 10 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → (∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦 → ∃𝑦 ∈ ω 𝐵𝑦))
27 isfi 8021 . . . . . . . . . 10 (𝐵 ∈ Fin ↔ ∃𝑦 ∈ ω 𝐵𝑦)
2826, 27syl6ibr 242 . . . . . . . . 9 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → (∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦𝐵 ∈ Fin))
2928adantl 481 . . . . . . . 8 ((𝑥 ∈ ω ∧ (𝑧:𝐴1-1-onto𝑥𝐵𝐴)) → (∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦𝐵 ∈ Fin))
3012, 29mpd 15 . . . . . . 7 ((𝑥 ∈ ω ∧ (𝑧:𝐴1-1-onto𝑥𝐵𝐴)) → 𝐵 ∈ Fin)
3130exp32 630 . . . . . 6 (𝑥 ∈ ω → (𝑧:𝐴1-1-onto𝑥 → (𝐵𝐴𝐵 ∈ Fin)))
3231exlimdv 1901 . . . . 5 (𝑥 ∈ ω → (∃𝑧 𝑧:𝐴1-1-onto𝑥 → (𝐵𝐴𝐵 ∈ Fin)))
332, 32syl5bi 232 . . . 4 (𝑥 ∈ ω → (𝐴𝑥 → (𝐵𝐴𝐵 ∈ Fin)))
3433rexlimiv 3056 . . 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 1744  wcel 2030  wrex 2942  wss 3607   class class class wbr 4685  ran crn 5144  cres 5145  cima 5146  1-1wf1 5923  ontowfo 5924  1-1-ontowf1o 5925  ωcom 7107  cen 7994  Fincfn 7997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-om 7108  df-er 7787  df-en 7998  df-fin 8001
This theorem is referenced by:  domfi  8222  ssfid  8224  infi  8225  finresfin  8227  diffi  8233  findcard3  8244  unfir  8269  fnfi  8279  fofinf1o  8282  cnvfi  8289  f1fi  8294  imafi  8300  mapfi  8303  ixpfi  8304  ixpfi2  8305  mptfi  8306  cnvimamptfin  8308  fisuppfi  8324  suppssfifsupp  8331  fsuppunbi  8337  snopfsupp  8339  fsuppres  8341  ressuppfi  8342  fsuppmptif  8346  fsuppco2  8349  fsuppcor  8350  sniffsupp  8356  elfiun  8377  wemapso2lem  8498  cantnfp1lem1  8613  oemapvali  8619  ackbij2lem1  9079  ackbij1lem11  9090  fin23lem26  9185  fin23lem23  9186  fin23lem21  9199  fin11a  9243  isfin1-3  9246  axcclem  9317  ssnn0fi  12824  hashun3  13211  hashss  13235  hashssdif  13238  hashsslei  13251  hashreshashfun  13264  hashbclem  13274  hashf1lem2  13278  seqcoll2  13287  pr2pwpr  13299  isercolllem2  14440  isercoll  14442  fsum2dlem  14545  fsumcom2OLD  14550  fsumless  14572  fsumabs  14577  fsumrlim  14587  fsumo1  14588  cvgcmpce  14594  fsumiun  14597  qshash  14603  incexclem  14612  incexc  14613  incexc2  14614  fprod2dlem  14754  fprodcom2OLD  14759  fprodmodd  14772  sumeven  15157  sumodd  15158  bitsfi  15206  bitsinv1  15211  bitsinvp1  15218  sadcaddlem  15226  sadadd2lem  15228  sadadd3  15230  sadaddlem  15235  sadasslem  15239  sadeq  15241  phicl2  15520  phibnd  15523  hashdvds  15527  phiprmpw  15528  phimullem  15531  eulerthlem2  15534  eulerth  15535  phisum  15542  sumhash  15647  prmreclem2  15668  prmreclem3  15669  prmreclem4  15670  prmreclem5  15671  1arith  15678  4sqlem11  15706  vdwlem11  15742  hashbccl  15754  ramlb  15770  0ram  15771  ramub1lem1  15777  ramub1lem2  15778  prmgaplem3  15804  prmgaplem4  15805  isstruct2  15914  lagsubg2  17702  lagsubg  17703  orbsta2  17793  symgbasfi  17852  symgfisg  17934  symggen2  17937  odcl2  18028  oddvds2  18029  sylow1lem2  18060  sylow1lem3  18061  sylow1lem4  18062  sylow1lem5  18063  odcau  18065  pgpssslw  18075  sylow2alem2  18079  sylow2a  18080  sylow2blem1  18081  sylow2blem3  18083  slwhash  18085  fislw  18086  sylow2  18087  sylow3lem1  18088  sylow3lem3  18090  sylow3lem4  18091  sylow3lem6  18093  cyggenod  18332  gsumval3lem1  18352  gsumval3lem2  18353  gsumval3  18354  gsumzadd  18368  gsumpt  18407  gsum2dlem1  18415  gsum2dlem2  18416  gsum2d  18417  gsum2d2lem  18418  dprdfadd  18465  ablfacrplem  18510  ablfacrp2  18512  ablfac1c  18516  ablfac1eulem  18517  ablfac1eu  18518  pgpfac1lem5  18524  pgpfaclem2  18527  pgpfaclem3  18528  ablfaclem3  18532  lcomfsupp  18951  psrbaglecl  19417  psrbagaddcl  19418  psrbagcon  19419  mplsubg  19485  mpllss  19486  mplcoe5  19516  psrbagsn  19543  psr1baslem  19603  dsmmfi  20130  dsmmacl  20133  dsmmsubg  20135  dsmmlss  20136  frlmsslsp  20183  mamures  20244  submabas  20432  mdetdiaglem  20452  mdetrlin  20456  mdetrsca  20457  mdetralt  20462  maducoeval2  20494  madugsum  20497  fctop  20856  restfpw  21031  fincmp  21244  cmpfi  21259  bwth  21261  finlocfin  21371  lfinpfin  21375  locfincmp  21377  1stckgenlem  21404  ptbasfi  21432  ptcnplem  21472  ptcmpfi  21664  cfinfil  21744  ufinffr  21780  fin1aufil  21783  tsmsres  21994  xrge0gsumle  22683  xrge0tsms  22684  fsumcn  22720  rrxcph  23226  rrxmval  23234  ovoliunlem1  23316  ovolicc2lem4  23334  ovolicc2lem5  23335  i1fima  23490  i1fd  23493  itg1cl  23497  itg1ge0  23498  i1f0  23499  i1f1  23502  i1fadd  23507  i1fmul  23508  itg1addlem4  23511  i1fmulc  23515  itg1mulc  23516  i1fres  23517  itg10a  23522  itg1ge0a  23523  itg1climres  23526  mbfi1fseqlem4  23530  itgfsum  23638  dvmptfsum  23783  plyexmo  24113  aannenlem2  24129  aalioulem2  24133  birthday  24726  jensenlem1  24758  jensenlem2  24759  jensen  24760  wilthlem2  24840  ppifi  24877  prmdvdsfi  24878  0sgm  24915  sgmf  24916  sgmnncl  24918  ppiprm  24922  chtprm  24924  chtdif  24929  efchtdvds  24930  ppidif  24934  ppiltx  24948  mumul  24952  sqff1o  24953  fsumdvdsdiag  24955  fsumdvdscom  24956  dvdsflsumcom  24959  musum  24962  musumsum  24963  muinv  24964  fsumdvdsmul  24966  ppiub  24974  vmasum  24986  logfac2  24987  perfectlem2  25000  dchrfi  25025  dchrabs  25030  dchrptlem1  25034  dchrptlem2  25035  dchrpt  25037  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  chebbnd1lem1  25203  chtppilimlem1  25207  rplogsumlem2  25219  rpvmasumlem  25221  dchrvmasumlem1  25229  dchrisum0ff  25241  rpvmasum2  25246  dchrisum0re  25247  dchrisum0  25254  rplogsum  25261  dirith2  25262  vmalogdivsum2  25272  logsqvma  25276  logsqvma2  25277  selberg  25282  selberg34r  25305  pntsval2  25310  pntrlog2bndlem1  25311  cusgrfi  26410  wwlksnfi  26869  hashwwlksnext  26877  relfi  29541  imafi2  29617  unifi3  29618  ffsrn  29632  gsumle  29907  xrge0tsmsd  29913  hasheuni  30275  carsgclctunlem1  30507  sibfof  30530  sitgclg  30532  oddpwdc  30544  eulerpartlems  30550  eulerpartlemb  30558  eulerpartlemmf  30565  eulerpartlemgf  30569  eulerpartlemgs2  30570  coinfliplem  30668  coinflippv  30673  ballotlemfelz  30680  ballotlemfp1  30681  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemiex  30691  ballotlemsup  30694  ballotlemfg  30715  ballotlemfrc  30716  ballotlemfrceq  30718  ballotth  30727  breprexpnat  30840  hgt750lemb  30862  hgt750leme  30864  deranglem  31274  subfacp1lem3  31290  subfacp1lem5  31292  subfacp1lem6  31293  erdszelem2  31300  erdszelem8  31306  erdsze2lem2  31312  snmlff  31437  mvrsfpw  31529  finminlem  32437  topdifinffinlem  33325  matunitlindflem1  33535  poimirlem9  33548  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem30  33569  poimirlem32  33571  itg2addnclem2  33592  nnubfi  33676  nninfnub  33677  sstotbnd2  33703  cntotbnd  33725  rencldnfilem  37701  jm2.22  37879  jm2.23  37880  filnm  37977  pwssfi  39525  disjinfi  39694  fsumiunss  40125  fprodexp  40144  fprodabs2  40145  mccllem  40147  sumnnodd  40180  fprodcncf  40432  dvmptfprod  40478  dvnprodlem1  40479  dvnprodlem2  40480  fourierdlem25  40667  fourierdlem37  40679  fourierdlem51  40692  fourierdlem79  40720  fouriersw  40766  etransclem16  40785  etransclem24  40793  etransclem33  40802  etransclem44  40813  sge0resplit  40941  sge0iunmptlemfi  40948  sge0iunmptlemre  40950  carageniuncllem2  41057  hsphoidmvle2  41120  hsphoidmvle  41121  hoidmvlelem4  41133  hoidmvlelem5  41134  fmtnoinf  41773  perfectALTVlem2  41956  rmsuppfi  42479  mndpsuppfi  42481  scmsuppfi  42483  suppmptcfin  42485
  Copyright terms: Public domain W3C validator