Theorem ssfi 8429

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.

Step	Hyp	Ref	Expression
1		isfi 8226	. . 3 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
2		bren 8211	. . . . 5 ⊢ (𝐴 ≈ 𝑥 ↔ ∃𝑧 𝑧:𝐴–1-1-onto→𝑥)
3		f1ofo 6370	. . . . . . . . . . 11 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–onto→𝑥)
4		imassrn 5701	. . . . . . . . . . . 12 ⊢ (𝑧 “ 𝐵) ⊆ ran 𝑧
5		forn 6344	. . . . . . . . . . . 12 ⊢ (𝑧:𝐴–onto→𝑥 → ran 𝑧 = 𝑥)
6	4, 5	syl5sseq 3861	. . . . . . . . . . 11 ⊢ (𝑧:𝐴–onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥)
7	3, 6	syl 17	. . . . . . . . . 10 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥)
8		ssnnfi 8428	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ω ∧ (𝑧 “ 𝐵) ⊆ 𝑥) → (𝑧 “ 𝐵) ∈ Fin)
9		isfi 8226	. . . . . . . . . . 11 ⊢ ((𝑧 “ 𝐵) ∈ Fin ↔ ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
10	8, 9	sylib 209	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ω ∧ (𝑧 “ 𝐵) ⊆ 𝑥) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
11	7, 10	sylan2 582	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ 𝑧:𝐴–1-1-onto→𝑥) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
12	11	adantrr 699	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
13		f1of1 6362	. . . . . . . . . . . . . 14 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–1-1→𝑥)
14		f1ores 6377	. . . . . . . . . . . . . 14 ⊢ ((𝑧:𝐴–1-1→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵))
15	13, 14	sylan 571	. . . . . . . . . . . . 13 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵))
16		vex 3405	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
17	16	resex 5662	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ↾ 𝐵) ∈ V
18		f1oeq1 6353	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑧 ↾ 𝐵) → (𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵) ↔ (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵)))
19	17, 18	spcev 3504	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵))
20		bren 8211	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≈ (𝑧 “ 𝐵) ↔ ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵))
21	19, 20	sylibr 225	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → 𝐵 ≈ (𝑧 “ 𝐵))
22		entr 8254	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ≈ (𝑧 “ 𝐵) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
23	21, 22	sylan 571	. . . . . . . . . . . . 13 ⊢ (((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
24	15, 23	sylan 571	. . . . . . . . . . . 12 ⊢ (((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
25	24	ex 399	. . . . . . . . . . 11 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → ((𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ≈ 𝑦))
26	25	reximdv 3214	. . . . . . . . . 10 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → ∃𝑦 ∈ ω 𝐵 ≈ 𝑦))
27		isfi 8226	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin ↔ ∃𝑦 ∈ ω 𝐵 ≈ 𝑦)
28	26, 27	syl6ibr 243	. . . . . . . . 9 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ∈ Fin))
29	28	adantl 469	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ∈ Fin))
30	12, 29	mpd 15	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → 𝐵 ∈ Fin)
31	30	exp32 409	. . . . . 6 ⊢ (𝑥 ∈ ω → (𝑧:𝐴–1-1-onto→𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
32	31	exlimdv 2024	. . . . 5 ⊢ (𝑥 ∈ ω → (∃𝑧 𝑧:𝐴–1-1-onto→𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
33	2, 32	syl5bi 233	. . . 4 ⊢ (𝑥 ∈ ω → (𝐴 ≈ 𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
34	33	rexlimiv 3226	. . 3 ⊢ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))
35	1, 34	sylbi 208	. 2 ⊢ (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))
36	35	imp 395	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 384  ∃wex 1859   ∈ wcel 2157  ∃wrex 3108   ⊆ wss 3780   class class class wbr 4855  ran crn 5325   ↾ cres 5326   “ cima 5327  –1-1→wf1 6108  –onto→wfo 6109  –1-1-onto→wf1o 6110  ωcom 7305   ≈ cen 8199  Fincfn 8202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-om 7306  df-er 7989  df-en 8203  df-fin 8206

This theorem is referenced by:  domfi  8430  ssfid  8432  infi  8433  finresfin  8435  diffi  8441  findcard3  8452  unfir  8477  fnfi  8487  fofinf1o  8490  cnvfi  8497  f1fi  8502  imafi  8508  mapfi  8511  ixpfi  8512  ixpfi2  8513  mptfi  8514  cnvimamptfin  8516  fisuppfi  8532  suppssfifsupp  8539  fsuppunbi  8545  snopfsupp  8547  fsuppres  8549  ressuppfi  8550  fsuppmptif  8554  fsuppco2  8557  fsuppcor  8558  sniffsupp  8564  elfiun  8585  wemapso2lem  8706  cantnfp1lem1  8832  oemapvali  8838  ackbij2lem1  9336  ackbij1lem11  9347  fin23lem26  9442  fin23lem23  9443  fin23lem21  9456  fin11a  9500  isfin1-3  9503  axcclem  9574  ssnn0fi  13028  hashun3  13411  hashss  13434  hashssdif  13437  hashsslei  13450  hashreshashfun  13463  hashbclem  13473  hashf1lem2  13477  seqcoll2  13486  pr2pwpr  13498  isercolllem2  14639  isercoll  14641  fsum2dlem  14744  fsumless  14770  fsumabs  14775  fsumrlim  14785  fsumo1  14786  cvgcmpce  14792  fsumiun  14795  qshash  14801  incexclem  14810  incexc  14811  incexc2  14812  fprod2dlem  14951  fprodmodd  14968  sumeven  15350  sumodd  15351  bitsfi  15398  bitsinv1  15403  bitsinvp1  15410  sadcaddlem  15418  sadadd2lem  15420  sadadd3  15422  sadaddlem  15427  sadasslem  15431  sadeq  15433  phicl2  15710  phibnd  15713  hashdvds  15717  phiprmpw  15718  phimullem  15721  eulerthlem2  15724  eulerth  15725  phisum  15732  sumhash  15837  prmreclem2  15858  prmreclem3  15859  prmreclem4  15860  prmreclem5  15861  1arith  15868  4sqlem11  15896  vdwlem11  15932  hashbccl  15944  ramlb  15960  0ram  15961  ramub1lem1  15967  ramub1lem2  15968  prmgaplem3  15994  prmgaplem4  15995  isstruct2  16098  lagsubg2  17877  lagsubg  17878  orbsta2  17968  symgbasfi  18027  symgfisg  18109  symggen2  18112  odcl2  18203  oddvds2  18204  sylow1lem2  18235  sylow1lem3  18236  sylow1lem4  18237  sylow1lem5  18238  odcau  18240  pgpssslw  18250  sylow2alem2  18254  sylow2a  18255  sylow2blem1  18256  sylow2blem3  18258  slwhash  18260  fislw  18261  sylow2  18262  sylow3lem1  18263  sylow3lem3  18265  sylow3lem4  18266  sylow3lem6  18268  cyggenod  18507  gsumval3lem1  18527  gsumval3lem2  18528  gsumval3  18529  gsumzadd  18543  gsumpt  18582  gsum2dlem1  18590  gsum2dlem2  18591  gsum2d  18592  gsum2d2lem  18593  dprdfadd  18641  ablfacrplem  18686  ablfacrp2  18688  ablfac1c  18692  ablfac1eulem  18693  ablfac1eu  18694  pgpfac1lem5  18700  pgpfaclem2  18703  pgpfaclem3  18704  ablfaclem3  18708  lcomfsupp  19127  psrbaglecl  19598  psrbagaddcl  19599  psrbagcon  19600  mplsubg  19666  mpllss  19667  mplcoe5  19697  psrbagsn  19723  psr1baslem  19783  dsmmfi  20313  dsmmacl  20316  dsmmsubg  20318  dsmmlss  20319  frlmsslsp  20366  mamures  20427  submabas  20616  mdetdiaglem  20636  mdetrlin  20640  mdetrsca  20641  mdetralt  20646  maducoeval2  20678  madugsum  20681  fctop  21043  restfpw  21218  fincmp  21431  cmpfi  21446  bwth  21448  finlocfin  21558  lfinpfin  21562  locfincmp  21564  1stckgenlem  21591  ptbasfi  21619  ptcnplem  21659  ptcmpfi  21851  cfinfil  21931  ufinffr  21967  fin1aufil  21970  tsmsres  22181  xrge0gsumle  22870  xrge0tsms  22871  fsumcn  22907  rrxcph  23415  rrxmval  23423  ovoliunlem1  23506  ovolicc2lem4  23524  ovolicc2lem5  23525  i1fima  23682  i1fd  23685  itg1cl  23689  itg1ge0  23690  i1f0  23691  i1f1  23694  i1fadd  23699  i1fmul  23700  itg1addlem4  23703  i1fmulc  23707  itg1mulc  23708  i1fres  23709  itg10a  23714  itg1ge0a  23715  itg1climres  23718  mbfi1fseqlem4  23722  itgfsum  23830  dvmptfsum  23975  plyexmo  24305  aannenlem2  24321  aalioulem2  24325  birthday  24918  jensenlem1  24950  jensenlem2  24951  jensen  24952  wilthlem2  25032  ppifi  25069  prmdvdsfi  25070  0sgm  25107  sgmf  25108  sgmnncl  25110  ppiprm  25114  chtprm  25116  chtdif  25121  efchtdvds  25122  ppidif  25126  ppiltx  25140  mumul  25144  sqff1o  25145  fsumdvdsdiag  25147  fsumdvdscom  25148  dvdsflsumcom  25151  musum  25154  musumsum  25155  muinv  25156  fsumdvdsmul  25158  ppiub  25166  vmasum  25178  logfac2  25179  perfectlem2  25192  dchrfi  25217  dchrabs  25222  dchrptlem1  25226  dchrptlem2  25227  dchrpt  25229  lgsquadlem1  25342  lgsquadlem2  25343  lgsquadlem3  25344  chebbnd1lem1  25395  chtppilimlem1  25399  rplogsumlem2  25411  rpvmasumlem  25413  dchrvmasumlem1  25421  dchrisum0ff  25433  rpvmasum2  25438  dchrisum0re  25439  dchrisum0  25446  rplogsum  25453  dirith2  25454  vmalogdivsum2  25464  logsqvma  25468  logsqvma2  25469  selberg  25474  selberg34r  25497  pntsval2  25502  pntrlog2bndlem1  25503  cusgrfi  26605  wwlksnfi  27066  hashwwlksnext  27075  relfi  29763  imafi2  29839  unifi3  29840  ffsrn  29854  gsumle  30127  xrge0tsmsd  30133  hasheuni  30495  carsgclctunlem1  30727  sibfof  30750  sitgclg  30752  oddpwdc  30764  eulerpartlems  30770  eulerpartlemb  30778  eulerpartlemmf  30785  eulerpartlemgf  30789  eulerpartlemgs2  30790  coinfliplem  30888  coinflippv  30893  ballotlemfelz  30900  ballotlemfp1  30901  ballotlemfc0  30902  ballotlemfcc  30903  ballotlemiex  30911  ballotlemsup  30914  ballotlemfg  30935  ballotlemfrc  30936  ballotlemfrceq  30938  ballotth  30947  breprexpnat  31060  hgt750lemb  31082  hgt750leme  31084  deranglem  31493  subfacp1lem3  31509  subfacp1lem5  31511  subfacp1lem6  31512  erdszelem2  31519  erdszelem8  31525  erdsze2lem2  31531  snmlff  31656  mvrsfpw  31748  finminlem  32655  topdifinffinlem  33530  matunitlindflem1  33737  poimirlem9  33750  poimirlem26  33767  poimirlem27  33768  poimirlem28  33769  poimirlem30  33771  poimirlem32  33773  itg2addnclem2  33793  nnubfi  33876  nninfnub  33877  sstotbnd2  33903  cntotbnd  33925  rencldnfilem  37904  jm2.22  38081  jm2.23  38082  filnm  38179  pwssfi  39722  disjinfi  39887  fsumiunss  40305  fprodexp  40324  fprodabs2  40325  mccllem  40327  sumnnodd  40360  fprodcncf  40612  dvmptfprod  40658  dvnprodlem1  40659  dvnprodlem2  40660  fourierdlem25  40846  fourierdlem37  40858  fourierdlem51  40871  fourierdlem79  40899  fouriersw  40945  etransclem16  40964  etransclem24  40972  etransclem33  40981  etransclem44  40992  sge0resplit  41120  sge0iunmptlemfi  41127  sge0iunmptlemre  41129  carageniuncllem2  41236  hsphoidmvle2  41299  hsphoidmvle  41300  hoidmvlelem4  41312  hoidmvlelem5  41313  fmtnoinf  42041  perfectALTVlem2  42224  rmsuppfi  42740  mndpsuppfi  42742  scmsuppfi  42744  suppmptcfin  42746