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

Theorem ssfi 8727
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 8522 . . 3 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
2 bren 8507 . . . . 5 (𝐴𝑥 ↔ ∃𝑧 𝑧:𝐴1-1-onto𝑥)
3 f1ofo 6616 . . . . . . . . . . 11 (𝑧:𝐴1-1-onto𝑥𝑧:𝐴onto𝑥)
4 imassrn 5934 . . . . . . . . . . . 12 (𝑧𝐵) ⊆ ran 𝑧
5 forn 6587 . . . . . . . . . . . 12 (𝑧:𝐴onto𝑥 → ran 𝑧 = 𝑥)
64, 5sseqtrid 4018 . . . . . . . . . . 11 (𝑧:𝐴onto𝑥 → (𝑧𝐵) ⊆ 𝑥)
73, 6syl 17 . . . . . . . . . 10 (𝑧:𝐴1-1-onto𝑥 → (𝑧𝐵) ⊆ 𝑥)
8 ssnnfi 8726 . . . . . . . . . . 11 ((𝑥 ∈ ω ∧ (𝑧𝐵) ⊆ 𝑥) → (𝑧𝐵) ∈ Fin)
9 isfi 8522 . . . . . . . . . . 11 ((𝑧𝐵) ∈ Fin ↔ ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
108, 9sylib 219 . . . . . . . . . 10 ((𝑥 ∈ ω ∧ (𝑧𝐵) ⊆ 𝑥) → ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
117, 10sylan2 592 . . . . . . . . 9 ((𝑥 ∈ ω ∧ 𝑧:𝐴1-1-onto𝑥) → ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
1211adantrr 713 . . . . . . . 8 ((𝑥 ∈ ω ∧ (𝑧:𝐴1-1-onto𝑥𝐵𝐴)) → ∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦)
13 f1of1 6608 . . . . . . . . . . . . . 14 (𝑧:𝐴1-1-onto𝑥𝑧:𝐴1-1𝑥)
14 f1ores 6623 . . . . . . . . . . . . . 14 ((𝑧:𝐴1-1𝑥𝐵𝐴) → (𝑧𝐵):𝐵1-1-onto→(𝑧𝐵))
1513, 14sylan 580 . . . . . . . . . . . . 13 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → (𝑧𝐵):𝐵1-1-onto→(𝑧𝐵))
16 vex 3498 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
1716resex 5893 . . . . . . . . . . . . . . . 16 (𝑧𝐵) ∈ V
18 f1oeq1 6598 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑧𝐵) → (𝑥:𝐵1-1-onto→(𝑧𝐵) ↔ (𝑧𝐵):𝐵1-1-onto→(𝑧𝐵)))
1917, 18spcev 3606 . . . . . . . . . . . . . . 15 ((𝑧𝐵):𝐵1-1-onto→(𝑧𝐵) → ∃𝑥 𝑥:𝐵1-1-onto→(𝑧𝐵))
20 bren 8507 . . . . . . . . . . . . . . 15 (𝐵 ≈ (𝑧𝐵) ↔ ∃𝑥 𝑥:𝐵1-1-onto→(𝑧𝐵))
2119, 20sylibr 235 . . . . . . . . . . . . . 14 ((𝑧𝐵):𝐵1-1-onto→(𝑧𝐵) → 𝐵 ≈ (𝑧𝐵))
22 entr 8550 . . . . . . . . . . . . . 14 ((𝐵 ≈ (𝑧𝐵) ∧ (𝑧𝐵) ≈ 𝑦) → 𝐵𝑦)
2321, 22sylan 580 . . . . . . . . . . . . 13 (((𝑧𝐵):𝐵1-1-onto→(𝑧𝐵) ∧ (𝑧𝐵) ≈ 𝑦) → 𝐵𝑦)
2415, 23sylan 580 . . . . . . . . . . . 12 (((𝑧:𝐴1-1-onto𝑥𝐵𝐴) ∧ (𝑧𝐵) ≈ 𝑦) → 𝐵𝑦)
2524ex 413 . . . . . . . . . . 11 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → ((𝑧𝐵) ≈ 𝑦𝐵𝑦))
2625reximdv 3273 . . . . . . . . . 10 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → (∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦 → ∃𝑦 ∈ ω 𝐵𝑦))
27 isfi 8522 . . . . . . . . . 10 (𝐵 ∈ Fin ↔ ∃𝑦 ∈ ω 𝐵𝑦)
2826, 27syl6ibr 253 . . . . . . . . 9 ((𝑧:𝐴1-1-onto𝑥𝐵𝐴) → (∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦𝐵 ∈ Fin))
2928adantl 482 . . . . . . . 8 ((𝑥 ∈ ω ∧ (𝑧:𝐴1-1-onto𝑥𝐵𝐴)) → (∃𝑦 ∈ ω (𝑧𝐵) ≈ 𝑦𝐵 ∈ Fin))
3012, 29mpd 15 . . . . . . 7 ((𝑥 ∈ ω ∧ (𝑧:𝐴1-1-onto𝑥𝐵𝐴)) → 𝐵 ∈ Fin)
3130exp32 421 . . . . . 6 (𝑥 ∈ ω → (𝑧:𝐴1-1-onto𝑥 → (𝐵𝐴𝐵 ∈ Fin)))
3231exlimdv 1925 . . . . 5 (𝑥 ∈ ω → (∃𝑧 𝑧:𝐴1-1-onto𝑥 → (𝐵𝐴𝐵 ∈ Fin)))
332, 32syl5bi 243 . . . 4 (𝑥 ∈ ω → (𝐴𝑥 → (𝐵𝐴𝐵 ∈ Fin)))
3433rexlimiv 3280 . . 3 (∃𝑥 ∈ ω 𝐴𝑥 → (𝐵𝐴𝐵 ∈ Fin))
351, 34sylbi 218 . 2 (𝐴 ∈ Fin → (𝐵𝐴𝐵 ∈ Fin))
3635imp 407 1 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wex 1771  wcel 2105  wrex 3139  wss 3935   class class class wbr 5058  ran crn 5550  cres 5551  cima 5552  1-1wf1 6346  ontowfo 6347  1-1-ontowf1o 6348  ωcom 7568  cen 8495  Fincfn 8498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  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 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  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 7569  df-er 8279  df-en 8499  df-fin 8502
This theorem is referenced by:  domfi  8728  ssfid  8730  infi  8731  finresfin  8733  diffi  8739  findcard3  8750  unfir  8775  fnfi  8785  fofinf1o  8788  cnvfi  8795  f1fi  8800  imafi  8806  mapfi  8809  ixpfi2  8811  mptfi  8812  cnvimamptfin  8814  suppssfifsupp  8837  snopfsupp  8845  fsuppres  8847  sniffsupp  8862  elfiun  8883  oemapvali  9136  ackbij2lem1  9630  ackbij1lem11  9641  fin23lem26  9736  fin23lem23  9737  fin23lem21  9750  fin11a  9794  isfin1-3  9797  axcclem  9868  ssnn0fi  13343  hashun3  13735  hashss  13760  hashssdif  13763  hashsslei  13777  hashreshashfun  13790  hashbclem  13800  hashf1lem2  13804  seqcoll2  13813  pr2pwpr  13827  fsumless  15141  cvgcmpce  15163  qshash  15172  incexclem  15181  incexc  15182  incexc2  15183  fprodmodd  15341  sumeven  15728  sumodd  15729  bitsfi  15776  bitsinv1  15781  bitsinvp1  15788  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  sadaddlem  15805  sadasslem  15809  sadeq  15811  phicl2  16095  phibnd  16098  hashdvds  16102  phiprmpw  16103  phimullem  16106  eulerthlem2  16109  eulerth  16110  phisum  16117  sumhash  16222  prmreclem2  16243  prmreclem3  16244  prmreclem4  16245  prmreclem5  16246  1arith  16253  hashbccl  16329  prmgaplem3  16379  lagsubg  18282  symgfisg  18527  symggen2  18530  odcl2  18623  sylow1lem2  18655  sylow1lem3  18656  sylow1lem4  18657  sylow1lem5  18658  pgpssslw  18670  sylow2alem2  18674  sylow2a  18675  sylow2blem3  18678  sylow3lem3  18685  sylow3lem6  18688  gsumval3lem1  18956  gsumval3lem2  18957  gsumval3  18958  gsumpt  19013  ablfacrplem  19118  ablfacrp2  19120  ablfac1c  19124  ablfac1eulem  19125  ablfac1eu  19126  mplsubg  20147  mpllss  20148  psrbagsn  20205  psr1baslem  20283  dsmmfi  20812  submabas  21117  mdetdiaglem  21137  maducoeval2  21179  fctop  21542  restfpw  21717  fincmp  21931  cmpfi  21946  bwth  21948  finlocfin  22058  lfinpfin  22062  locfincmp  22064  1stckgenlem  22091  ptbasfi  22119  ptcnplem  22159  ptcmpfi  22351  cfinfil  22431  ufinffr  22467  fin1aufil  22470  tsmsres  22681  ovoliunlem1  24032  ovolicc2lem4  24050  ovolicc2lem5  24051  i1fima  24208  i1fd  24211  itg1cl  24215  itg1ge0  24216  i1f0  24217  i1f1  24220  i1fmul  24226  itg1addlem4  24229  itg1mulc  24234  itg10a  24240  itg1ge0a  24241  itg1climres  24244  plyexmo  24831  aannenlem2  24847  aalioulem2  24851  birthday  25460  wilthlem2  25574  ppifi  25611  prmdvdsfi  25612  ppiprm  25656  chtprm  25658  chtdif  25663  efchtdvds  25664  ppidif  25668  ppiltx  25682  mumul  25686  sqff1o  25687  musum  25696  ppiub  25708  vmasum  25720  logfac2  25721  dchrabs  25764  dchrptlem1  25768  dchrptlem2  25769  dchrpt  25771  lgsquadlem1  25884  lgsquadlem2  25885  lgsquadlem3  25886  chebbnd1lem1  25973  chtppilimlem1  25977  rpvmasum2  26016  dchrisum0re  26017  rplogsum  26031  dirith2  26032  cusgrfi  27168  wwlksnfiOLD  27613  hashwwlksnext  27621  relfi  30281  imafi2  30374  unifi3  30375  ffsrn  30392  xrge0tsmsd  30620  gsumle  30653  rmfsupp2  30794  hasheuni  31244  carsgclctunlem1  31475  sibfof  31498  sitgclg  31500  oddpwdc  31512  eulerpartlems  31518  eulerpartlemb  31526  eulerpartlemmf  31533  eulerpartlemgf  31537  eulerpartlemgs2  31538  coinfliplem  31636  coinflippv  31641  ballotlemfelz  31648  ballotlemfp1  31649  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemiex  31659  ballotlemsup  31662  ballotlemfg  31683  ballotlemfrc  31684  ballotlemfrceq  31686  ballotth  31695  breprexpnat  31805  hgt750lemb  31827  hgt750leme  31829  fisshasheq  32250  deranglem  32311  subfacp1lem3  32327  subfacp1lem5  32329  subfacp1lem6  32330  erdszelem2  32337  erdszelem8  32343  erdsze2lem2  32349  snmlff  32474  mvrsfpw  32651  finminlem  33564  topdifinffinlem  34511  matunitlindflem1  34770  poimirlem9  34783  poimirlem26  34800  poimirlem27  34801  poimirlem28  34802  poimirlem30  34804  poimirlem32  34806  itg2addnclem2  34826  nnubfi  34908  nninfnub  34909  sstotbnd2  34935  cntotbnd  34957  rencldnfilem  39297  jm2.22  39472  jm2.23  39473  filnm  39570  pwssfi  41187  disjinfi  41334  fsumiunss  41736  fprodexp  41755  fprodabs2  41756  mccllem  41758  sumnnodd  41791  fprodcncf  42064  dvmptfprod  42110  dvnprodlem1  42111  dvnprodlem2  42112  fourierdlem25  42298  fourierdlem37  42310  fourierdlem51  42323  fourierdlem79  42351  fouriersw  42397  etransclem16  42416  etransclem24  42424  etransclem33  42433  etransclem44  42444  sge0resplit  42569  sge0iunmptlemfi  42576  sge0iunmptlemre  42578  carageniuncllem2  42685  hsphoidmvle2  42748  hsphoidmvle  42749  hoidmvlelem4  42761  hoidmvlelem5  42762  fmtnoinf  43545  perfectALTVlem2  43734  rmsuppfi  44319  mndpsuppfi  44321  scmsuppfi  44323  suppmptcfin  44325
  Copyright terms: Public domain W3C validator