Theorem ssfi 8738

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 8533	. . 3 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
2		bren 8518	. . . . 5 ⊢ (𝐴 ≈ 𝑥 ↔ ∃𝑧 𝑧:𝐴–1-1-onto→𝑥)
3		f1ofo 6622	. . . . . . . . . . 11 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–onto→𝑥)
4		imassrn 5940	. . . . . . . . . . . 12 ⊢ (𝑧 “ 𝐵) ⊆ ran 𝑧
5		forn 6593	. . . . . . . . . . . 12 ⊢ (𝑧:𝐴–onto→𝑥 → ran 𝑧 = 𝑥)
6	4, 5	sseqtrid 4019	. . . . . . . . . . 11 ⊢ (𝑧:𝐴–onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥)
7	3, 6	syl 17	. . . . . . . . . 10 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥)
8		ssnnfi 8737	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ω ∧ (𝑧 “ 𝐵) ⊆ 𝑥) → (𝑧 “ 𝐵) ∈ Fin)
9		isfi 8533	. . . . . . . . . . 11 ⊢ ((𝑧 “ 𝐵) ∈ Fin ↔ ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
10	8, 9	sylib 220	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ω ∧ (𝑧 “ 𝐵) ⊆ 𝑥) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
11	7, 10	sylan2 594	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ 𝑧:𝐴–1-1-onto→𝑥) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
12	11	adantrr 715	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
13		f1of1 6614	. . . . . . . . . . . . . 14 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–1-1→𝑥)
14		f1ores 6629	. . . . . . . . . . . . . 14 ⊢ ((𝑧:𝐴–1-1→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵))
15	13, 14	sylan 582	. . . . . . . . . . . . 13 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵))
16		vex 3497	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
17	16	resex 5899	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ↾ 𝐵) ∈ V
18		f1oeq1 6604	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑧 ↾ 𝐵) → (𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵) ↔ (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵)))
19	17, 18	spcev 3607	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵))
20		bren 8518	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≈ (𝑧 “ 𝐵) ↔ ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵))
21	19, 20	sylibr 236	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → 𝐵 ≈ (𝑧 “ 𝐵))
22		entr 8561	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ≈ (𝑧 “ 𝐵) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
23	21, 22	sylan 582	. . . . . . . . . . . . 13 ⊢ (((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
24	15, 23	sylan 582	. . . . . . . . . . . 12 ⊢ (((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
25	24	ex 415	. . . . . . . . . . 11 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → ((𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ≈ 𝑦))
26	25	reximdv 3273	. . . . . . . . . 10 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → ∃𝑦 ∈ ω 𝐵 ≈ 𝑦))
27		isfi 8533	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin ↔ ∃𝑦 ∈ ω 𝐵 ≈ 𝑦)
28	26, 27	syl6ibr 254	. . . . . . . . 9 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ∈ Fin))
29	28	adantl 484	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ∈ Fin))
30	12, 29	mpd 15	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → 𝐵 ∈ Fin)
31	30	exp32 423	. . . . . 6 ⊢ (𝑥 ∈ ω → (𝑧:𝐴–1-1-onto→𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
32	31	exlimdv 1934	. . . . 5 ⊢ (𝑥 ∈ ω → (∃𝑧 𝑧:𝐴–1-1-onto→𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
33	2, 32	syl5bi 244	. . . 4 ⊢ (𝑥 ∈ ω → (𝐴 ≈ 𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
34	33	rexlimiv 3280	. . 3 ⊢ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))
35	1, 34	sylbi 219	. 2 ⊢ (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))
36	35	imp 409	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∃wrex 3139   ⊆ wss 3936   class class class wbr 5066  ran crn 5556   ↾ cres 5557   “ cima 5558  –1-1→wf1 6352  –onto→wfo 6353  –1-1-onto→wf1o 6354  ωcom 7580   ≈ cen 8506  Fincfn 8509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  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 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-om 7581  df-er 8289  df-en 8510  df-fin 8513

This theorem is referenced by:  domfi  8739  ssfid  8741  infi  8742  finresfin  8744  diffi  8750  findcard3  8761  unfir  8786  fnfi  8796  fofinf1o  8799  cnvfi  8806  f1fi  8811  imafi  8817  mapfi  8820  ixpfi2  8822  mptfi  8823  cnvimamptfin  8825  suppssfifsupp  8848  snopfsupp  8856  fsuppres  8858  sniffsupp  8873  elfiun  8894  oemapvali  9147  ackbij2lem1  9641  ackbij1lem11  9652  fin23lem26  9747  fin23lem23  9748  fin23lem21  9761  fin11a  9805  isfin1-3  9808  axcclem  9879  ssnn0fi  13354  hashun3  13746  hashss  13771  hashssdif  13774  hashsslei  13788  hashreshashfun  13801  hashbclem  13811  hashf1lem2  13815  seqcoll2  13824  pr2pwpr  13838  fsumless  15151  cvgcmpce  15173  qshash  15182  incexclem  15191  incexc  15192  incexc2  15193  fprodmodd  15351  sumeven  15738  sumodd  15739  bitsfi  15786  bitsinv1  15791  bitsinvp1  15798  sadcaddlem  15806  sadadd2lem  15808  sadadd3  15810  sadaddlem  15815  sadasslem  15819  sadeq  15821  phicl2  16105  phibnd  16108  hashdvds  16112  phiprmpw  16113  phimullem  16116  eulerthlem2  16119  eulerth  16120  phisum  16127  sumhash  16232  prmreclem2  16253  prmreclem3  16254  prmreclem4  16255  prmreclem5  16256  1arith  16263  hashbccl  16339  prmgaplem3  16389  lagsubg  18342  symgfisg  18596  symggen2  18599  odcl2  18692  sylow1lem2  18724  sylow1lem3  18725  sylow1lem4  18726  sylow1lem5  18727  pgpssslw  18739  sylow2alem2  18743  sylow2a  18744  sylow2blem3  18747  sylow3lem3  18754  sylow3lem6  18757  gsumval3lem1  19025  gsumval3lem2  19026  gsumval3  19027  gsumpt  19082  ablfacrplem  19187  ablfacrp2  19189  ablfac1c  19193  ablfac1eulem  19194  ablfac1eu  19195  mplsubg  20217  mpllss  20218  psrbagsn  20275  psr1baslem  20353  dsmmfi  20882  submabas  21187  mdetdiaglem  21207  maducoeval2  21249  fctop  21612  restfpw  21787  fincmp  22001  cmpfi  22016  bwth  22018  finlocfin  22128  lfinpfin  22132  locfincmp  22134  1stckgenlem  22161  ptbasfi  22189  ptcnplem  22229  ptcmpfi  22421  cfinfil  22501  ufinffr  22537  fin1aufil  22540  tsmsres  22752  ovoliunlem1  24103  ovolicc2lem4  24121  ovolicc2lem5  24122  i1fima  24279  i1fd  24282  itg1cl  24286  itg1ge0  24287  i1f0  24288  i1f1  24291  i1fmul  24297  itg1addlem4  24300  itg1mulc  24305  itg10a  24311  itg1ge0a  24312  itg1climres  24315  plyexmo  24902  aannenlem2  24918  aalioulem2  24922  birthday  25532  wilthlem2  25646  ppifi  25683  prmdvdsfi  25684  ppiprm  25728  chtprm  25730  chtdif  25735  efchtdvds  25736  ppidif  25740  ppiltx  25754  mumul  25758  sqff1o  25759  musum  25768  ppiub  25780  vmasum  25792  logfac2  25793  dchrabs  25836  dchrptlem1  25840  dchrptlem2  25841  dchrpt  25843  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  chebbnd1lem1  26045  chtppilimlem1  26049  rpvmasum2  26088  dchrisum0re  26089  rplogsum  26103  dirith2  26104  cusgrfi  27240  wwlksnfiOLD  27685  hashwwlksnext  27693  relfi  30352  imafi2  30447  unifi3  30448  ffsrn  30465  xrge0tsmsd  30692  gsumle  30725  rmfsupp2  30866  hasheuni  31344  carsgclctunlem1  31575  sibfof  31598  sitgclg  31600  oddpwdc  31612  eulerpartlems  31618  eulerpartlemb  31626  eulerpartlemmf  31633  eulerpartlemgf  31637  eulerpartlemgs2  31638  coinfliplem  31736  coinflippv  31741  ballotlemfelz  31748  ballotlemfp1  31749  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemiex  31759  ballotlemsup  31762  ballotlemfg  31783  ballotlemfrc  31784  ballotlemfrceq  31786  ballotth  31795  breprexpnat  31905  hgt750lemb  31927  hgt750leme  31929  fisshasheq  32352  deranglem  32413  subfacp1lem3  32429  subfacp1lem5  32431  subfacp1lem6  32432  erdszelem2  32439  erdszelem8  32445  erdsze2lem2  32451  snmlff  32576  mvrsfpw  32753  finminlem  33666  topdifinffinlem  34631  matunitlindflem1  34903  poimirlem9  34916  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem30  34937  poimirlem32  34939  itg2addnclem2  34959  nnubfi  35040  nninfnub  35041  sstotbnd2  35067  cntotbnd  35089  rencldnfilem  39466  jm2.22  39641  jm2.23  39642  filnm  39739  pwssfi  41356  disjinfi  41503  fsumiunss  41905  fprodexp  41924  fprodabs2  41925  mccllem  41927  sumnnodd  41960  fprodcncf  42233  dvmptfprod  42279  dvnprodlem1  42280  dvnprodlem2  42281  fourierdlem25  42466  fourierdlem37  42478  fourierdlem51  42491  fourierdlem79  42519  fouriersw  42565  etransclem16  42584  etransclem24  42592  etransclem33  42601  etransclem44  42612  sge0resplit  42737  sge0iunmptlemfi  42744  sge0iunmptlemre  42746  carageniuncllem2  42853  hsphoidmvle2  42916  hsphoidmvle  42917  hoidmvlelem4  42929  hoidmvlelem5  42930  fmtnoinf  43747  perfectALTVlem2  43936  rmsuppfi  44470  mndpsuppfi  44472  scmsuppfi  44474  suppmptcfin  44476