Theorem ssfi 8591

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 8388	. . 3 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
2		bren 8373	. . . . 5 ⊢ (𝐴 ≈ 𝑥 ↔ ∃𝑧 𝑧:𝐴–1-1-onto→𝑥)
3		f1ofo 6497	. . . . . . . . . . 11 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–onto→𝑥)
4		imassrn 5824	. . . . . . . . . . . 12 ⊢ (𝑧 “ 𝐵) ⊆ ran 𝑧
5		forn 6468	. . . . . . . . . . . 12 ⊢ (𝑧:𝐴–onto→𝑥 → ran 𝑧 = 𝑥)
6	4, 5	sseqtrid 3946	. . . . . . . . . . 11 ⊢ (𝑧:𝐴–onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥)
7	3, 6	syl 17	. . . . . . . . . 10 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥)
8		ssnnfi 8590	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ω ∧ (𝑧 “ 𝐵) ⊆ 𝑥) → (𝑧 “ 𝐵) ∈ Fin)
9		isfi 8388	. . . . . . . . . . 11 ⊢ ((𝑧 “ 𝐵) ∈ Fin ↔ ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
10	8, 9	sylib 219	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ω ∧ (𝑧 “ 𝐵) ⊆ 𝑥) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
11	7, 10	sylan2 592	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ 𝑧:𝐴–1-1-onto→𝑥) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
12	11	adantrr 713	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
13		f1of1 6489	. . . . . . . . . . . . . 14 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–1-1→𝑥)
14		f1ores 6504	. . . . . . . . . . . . . 14 ⊢ ((𝑧:𝐴–1-1→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵))
15	13, 14	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵))
16		vex 3443	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
17	16	resex 5787	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ↾ 𝐵) ∈ V
18		f1oeq1 6479	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑧 ↾ 𝐵) → (𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵) ↔ (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵)))
19	17, 18	spcev 3551	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵))
20		bren 8373	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≈ (𝑧 “ 𝐵) ↔ ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵))
21	19, 20	sylibr 235	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → 𝐵 ≈ (𝑧 “ 𝐵))
22		entr 8416	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ≈ (𝑧 “ 𝐵) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
23	21, 22	sylan 580	. . . . . . . . . . . . 13 ⊢ (((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
24	15, 23	sylan 580	. . . . . . . . . . . 12 ⊢ (((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
25	24	ex 413	. . . . . . . . . . 11 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → ((𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ≈ 𝑦))
26	25	reximdv 3238	. . . . . . . . . 10 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → ∃𝑦 ∈ ω 𝐵 ≈ 𝑦))
27		isfi 8388	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin ↔ ∃𝑦 ∈ ω 𝐵 ≈ 𝑦)
28	26, 27	syl6ibr 253	. . . . . . . . 9 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ∈ Fin))
29	28	adantl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ∈ Fin))
30	12, 29	mpd 15	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → 𝐵 ∈ Fin)
31	30	exp32 421	. . . . . 6 ⊢ (𝑥 ∈ ω → (𝑧:𝐴–1-1-onto→𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
32	31	exlimdv 1915	. . . . 5 ⊢ (𝑥 ∈ ω → (∃𝑧 𝑧:𝐴–1-1-onto→𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
33	2, 32	syl5bi 243	. . . 4 ⊢ (𝑥 ∈ ω → (𝐴 ≈ 𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
34	33	rexlimiv 3245	. . 3 ⊢ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))
35	1, 34	sylbi 218	. 2 ⊢ (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))
36	35	imp 407	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1765   ∈ wcel 2083  ∃wrex 3108   ⊆ wss 3865   class class class wbr 4968  ran crn 5451   ↾ cres 5452   “ cima 5453  –1-1→wf1 6229  –onto→wfo 6230  –1-1-onto→wf1o 6231  ωcom 7443   ≈ cen 8361  Fincfn 8364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-om 7444  df-er 8146  df-en 8365  df-fin 8368

This theorem is referenced by:  domfi  8592  ssfid  8594  infi  8595  finresfin  8597  diffi  8603  findcard3  8614  unfir  8639  fnfi  8649  fofinf1o  8652  cnvfi  8659  f1fi  8664  imafi  8670  mapfi  8673  ixpfi2  8675  mptfi  8676  cnvimamptfin  8678  suppssfifsupp  8701  snopfsupp  8709  fsuppres  8711  sniffsupp  8726  elfiun  8747  oemapvali  9000  ackbij2lem1  9494  ackbij1lem11  9505  fin23lem26  9600  fin23lem23  9601  fin23lem21  9614  fin11a  9658  isfin1-3  9661  axcclem  9732  ssnn0fi  13207  hashun3  13597  hashss  13622  hashssdif  13625  hashsslei  13639  hashreshashfun  13652  hashbclem  13662  hashf1lem2  13666  seqcoll2  13675  pr2pwpr  13687  fsumless  14988  cvgcmpce  15010  qshash  15019  incexclem  15028  incexc  15029  incexc2  15030  fprodmodd  15188  sumeven  15575  sumodd  15576  bitsfi  15623  bitsinv1  15628  bitsinvp1  15635  sadcaddlem  15643  sadadd2lem  15645  sadadd3  15647  sadaddlem  15652  sadasslem  15656  sadeq  15658  phicl2  15938  phibnd  15941  hashdvds  15945  phiprmpw  15946  phimullem  15949  eulerthlem2  15952  eulerth  15953  phisum  15960  sumhash  16065  prmreclem2  16086  prmreclem3  16087  prmreclem4  16088  prmreclem5  16089  1arith  16096  hashbccl  16172  prmgaplem3  16222  lagsubg  18099  symgfisg  18331  symggen2  18334  odcl2  18426  sylow1lem2  18458  sylow1lem3  18459  sylow1lem4  18460  sylow1lem5  18461  pgpssslw  18473  sylow2alem2  18477  sylow2a  18478  sylow2blem3  18481  sylow3lem3  18488  sylow3lem6  18491  gsumval3lem1  18750  gsumval3lem2  18751  gsumval3  18752  gsumpt  18806  ablfacrplem  18908  ablfacrp2  18910  ablfac1c  18914  ablfac1eulem  18915  ablfac1eu  18916  mplsubg  19909  mpllss  19910  psrbagsn  19966  psr1baslem  20040  dsmmfi  20568  submabas  20875  mdetdiaglem  20895  maducoeval2  20937  fctop  21300  restfpw  21475  fincmp  21689  cmpfi  21704  bwth  21706  finlocfin  21816  lfinpfin  21820  locfincmp  21822  1stckgenlem  21849  ptbasfi  21877  ptcnplem  21917  ptcmpfi  22109  cfinfil  22189  ufinffr  22225  fin1aufil  22228  tsmsres  22439  ovoliunlem1  23790  ovolicc2lem4  23808  ovolicc2lem5  23809  i1fima  23966  i1fd  23969  itg1cl  23973  itg1ge0  23974  i1f0  23975  i1f1  23978  i1fmul  23984  itg1addlem4  23987  itg1mulc  23992  itg10a  23998  itg1ge0a  23999  itg1climres  24002  plyexmo  24589  aannenlem2  24605  aalioulem2  24609  birthday  25218  wilthlem2  25332  ppifi  25369  prmdvdsfi  25370  ppiprm  25414  chtprm  25416  chtdif  25421  efchtdvds  25422  ppidif  25426  ppiltx  25440  mumul  25444  sqff1o  25445  musum  25454  ppiub  25466  vmasum  25478  logfac2  25479  dchrabs  25522  dchrptlem1  25526  dchrptlem2  25527  dchrpt  25529  lgsquadlem1  25642  lgsquadlem2  25643  lgsquadlem3  25644  chebbnd1lem1  25731  chtppilimlem1  25735  rpvmasum2  25774  dchrisum0re  25775  rplogsum  25789  dirith2  25790  cusgrfi  26927  wwlksnfiOLD  27371  hashwwlksnext  27379  relfi  30038  imafi2  30131  unifi3  30132  ffsrn  30149  gsumle  30490  xrge0tsmsd  30499  rmfsupp2  30516  hasheuni  30957  carsgclctunlem1  31188  sibfof  31211  sitgclg  31213  oddpwdc  31225  eulerpartlems  31231  eulerpartlemb  31239  eulerpartlemmf  31246  eulerpartlemgf  31250  eulerpartlemgs2  31251  coinfliplem  31349  coinflippv  31354  ballotlemfelz  31361  ballotlemfp1  31362  ballotlemfc0  31363  ballotlemfcc  31364  ballotlemiex  31372  ballotlemsup  31375  ballotlemfg  31396  ballotlemfrc  31397  ballotlemfrceq  31399  ballotth  31408  breprexpnat  31518  hgt750lemb  31540  hgt750leme  31542  fisshasheq  31962  deranglem  32023  subfacp1lem3  32039  subfacp1lem5  32041  subfacp1lem6  32042  erdszelem2  32049  erdszelem8  32055  erdsze2lem2  32061  snmlff  32186  mvrsfpw  32363  finminlem  33277  topdifinffinlem  34180  matunitlindflem1  34440  poimirlem9  34453  poimirlem26  34470  poimirlem27  34471  poimirlem28  34472  poimirlem30  34474  poimirlem32  34476  itg2addnclem2  34496  nnubfi  34578  nninfnub  34579  sstotbnd2  34605  cntotbnd  34627  rencldnfilem  38923  jm2.22  39098  jm2.23  39099  filnm  39196  pwssfi  40867  disjinfi  41015  fsumiunss  41419  fprodexp  41438  fprodabs2  41439  mccllem  41441  sumnnodd  41474  fprodcncf  41747  dvmptfprod  41793  dvnprodlem1  41794  dvnprodlem2  41795  fourierdlem25  41981  fourierdlem37  41993  fourierdlem51  42006  fourierdlem79  42034  fouriersw  42080  etransclem16  42099  etransclem24  42107  etransclem33  42116  etransclem44  42127  sge0resplit  42252  sge0iunmptlemfi  42259  sge0iunmptlemre  42261  carageniuncllem2  42368  hsphoidmvle2  42431  hsphoidmvle  42432  hoidmvlelem4  42444  hoidmvlelem5  42445  fmtnoinf  43202  perfectALTVlem2  43391  rmsuppfi  43923  mndpsuppfi  43925  scmsuppfi  43927  suppmptcfin  43929