Theorem ssfi 8740

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 8535	. . 3 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
2		bren 8520	. . . . 5 ⊢ (𝐴 ≈ 𝑥 ↔ ∃𝑧 𝑧:𝐴–1-1-onto→𝑥)
3		f1ofo 6624	. . . . . . . . . . 11 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–onto→𝑥)
4		imassrn 5942	. . . . . . . . . . . 12 ⊢ (𝑧 “ 𝐵) ⊆ ran 𝑧
5		forn 6595	. . . . . . . . . . . 12 ⊢ (𝑧:𝐴–onto→𝑥 → ran 𝑧 = 𝑥)
6	4, 5	sseqtrid 4021	. . . . . . . . . . 11 ⊢ (𝑧:𝐴–onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥)
7	3, 6	syl 17	. . . . . . . . . 10 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥)
8		ssnnfi 8739	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ω ∧ (𝑧 “ 𝐵) ⊆ 𝑥) → (𝑧 “ 𝐵) ∈ Fin)
9		isfi 8535	. . . . . . . . . . 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 6616	. . . . . . . . . . . . . 14 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–1-1→𝑥)
14		f1ores 6631	. . . . . . . . . . . . . 14 ⊢ ((𝑧:𝐴–1-1→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵))
15	13, 14	sylan 582	. . . . . . . . . . . . 13 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵))
16		vex 3499	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
17	16	resex 5901	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ↾ 𝐵) ∈ V
18		f1oeq1 6606	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑧 ↾ 𝐵) → (𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵) ↔ (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵)))
19	17, 18	spcev 3609	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵))
20		bren 8520	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≈ (𝑧 “ 𝐵) ↔ ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵))
21	19, 20	sylibr 236	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → 𝐵 ≈ (𝑧 “ 𝐵))
22		entr 8563	. . . . . . . . . . . . . 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 3275	. . . . . . . . . 10 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → ∃𝑦 ∈ ω 𝐵 ≈ 𝑦))
27		isfi 8535	. . . . . . . . . 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 3282	. . 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 3141   ⊆ wss 3938   class class class wbr 5068  ran crn 5558   ↾ cres 5559   “ cima 5560  –1-1→wf1 6354  –onto→wfo 6355  –1-1-onto→wf1o 6356  ωcom 7582   ≈ cen 8508  Fincfn 8511

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 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-om 7583  df-er 8291  df-en 8512  df-fin 8515

This theorem is referenced by:  domfi  8741  ssfid  8743  infi  8744  finresfin  8746  diffi  8752  findcard3  8763  unfir  8788  fnfi  8798  fofinf1o  8801  cnvfi  8808  f1fi  8813  imafi  8819  mapfi  8822  ixpfi2  8824  mptfi  8825  cnvimamptfin  8827  suppssfifsupp  8850  snopfsupp  8858  fsuppres  8860  sniffsupp  8875  elfiun  8896  oemapvali  9149  ackbij2lem1  9643  ackbij1lem11  9654  fin23lem26  9749  fin23lem23  9750  fin23lem21  9763  fin11a  9807  isfin1-3  9810  axcclem  9881  ssnn0fi  13356  hashun3  13748  hashss  13773  hashssdif  13776  hashsslei  13790  hashreshashfun  13803  hashbclem  13813  hashf1lem2  13817  seqcoll2  13826  pr2pwpr  13840  fsumless  15153  cvgcmpce  15175  qshash  15184  incexclem  15193  incexc  15194  incexc2  15195  fprodmodd  15353  sumeven  15740  sumodd  15741  bitsfi  15788  bitsinv1  15793  bitsinvp1  15800  sadcaddlem  15808  sadadd2lem  15810  sadadd3  15812  sadaddlem  15817  sadasslem  15821  sadeq  15823  phicl2  16107  phibnd  16110  hashdvds  16114  phiprmpw  16115  phimullem  16118  eulerthlem2  16121  eulerth  16122  phisum  16129  sumhash  16234  prmreclem2  16255  prmreclem3  16256  prmreclem4  16257  prmreclem5  16258  1arith  16265  hashbccl  16341  prmgaplem3  16391  lagsubg  18344  symgfisg  18598  symggen2  18601  odcl2  18694  sylow1lem2  18726  sylow1lem3  18727  sylow1lem4  18728  sylow1lem5  18729  pgpssslw  18741  sylow2alem2  18745  sylow2a  18746  sylow2blem3  18749  sylow3lem3  18756  sylow3lem6  18759  gsumval3lem1  19027  gsumval3lem2  19028  gsumval3  19029  gsumpt  19084  ablfacrplem  19189  ablfacrp2  19191  ablfac1c  19195  ablfac1eulem  19196  ablfac1eu  19197  mplsubg  20219  mpllss  20220  psrbagsn  20277  psr1baslem  20355  dsmmfi  20884  submabas  21189  mdetdiaglem  21209  maducoeval2  21251  fctop  21614  restfpw  21789  fincmp  22003  cmpfi  22018  bwth  22020  finlocfin  22130  lfinpfin  22134  locfincmp  22136  1stckgenlem  22163  ptbasfi  22191  ptcnplem  22231  ptcmpfi  22423  cfinfil  22503  ufinffr  22539  fin1aufil  22542  tsmsres  22754  ovoliunlem1  24105  ovolicc2lem4  24123  ovolicc2lem5  24124  i1fima  24281  i1fd  24284  itg1cl  24288  itg1ge0  24289  i1f0  24290  i1f1  24293  i1fmul  24299  itg1addlem4  24302  itg1mulc  24307  itg10a  24313  itg1ge0a  24314  itg1climres  24317  plyexmo  24904  aannenlem2  24920  aalioulem2  24924  birthday  25534  wilthlem2  25648  ppifi  25685  prmdvdsfi  25686  ppiprm  25730  chtprm  25732  chtdif  25737  efchtdvds  25738  ppidif  25742  ppiltx  25756  mumul  25760  sqff1o  25761  musum  25770  ppiub  25782  vmasum  25794  logfac2  25795  dchrabs  25838  dchrptlem1  25842  dchrptlem2  25843  dchrpt  25845  lgsquadlem1  25958  lgsquadlem2  25959  lgsquadlem3  25960  chebbnd1lem1  26047  chtppilimlem1  26051  rpvmasum2  26090  dchrisum0re  26091  rplogsum  26105  dirith2  26106  cusgrfi  27242  wwlksnfiOLD  27687  hashwwlksnext  27695  relfi  30354  imafi2  30449  unifi3  30450  ffsrn  30467  xrge0tsmsd  30694  gsumle  30727  rmfsupp2  30868  hasheuni  31346  carsgclctunlem1  31577  sibfof  31600  sitgclg  31602  oddpwdc  31614  eulerpartlems  31620  eulerpartlemb  31628  eulerpartlemmf  31635  eulerpartlemgf  31639  eulerpartlemgs2  31640  coinfliplem  31738  coinflippv  31743  ballotlemfelz  31750  ballotlemfp1  31751  ballotlemfc0  31752  ballotlemfcc  31753  ballotlemiex  31761  ballotlemsup  31764  ballotlemfg  31785  ballotlemfrc  31786  ballotlemfrceq  31788  ballotth  31797  breprexpnat  31907  hgt750lemb  31929  hgt750leme  31931  fisshasheq  32354  deranglem  32415  subfacp1lem3  32431  subfacp1lem5  32433  subfacp1lem6  32434  erdszelem2  32441  erdszelem8  32447  erdsze2lem2  32453  snmlff  32578  mvrsfpw  32755  finminlem  33668  topdifinffinlem  34630  matunitlindflem1  34890  poimirlem9  34903  poimirlem26  34920  poimirlem27  34921  poimirlem28  34922  poimirlem30  34924  poimirlem32  34926  itg2addnclem2  34946  nnubfi  35027  nninfnub  35028  sstotbnd2  35054  cntotbnd  35076  rencldnfilem  39424  jm2.22  39599  jm2.23  39600  filnm  39697  pwssfi  41314  disjinfi  41461  fsumiunss  41863  fprodexp  41882  fprodabs2  41883  mccllem  41885  sumnnodd  41918  fprodcncf  42191  dvmptfprod  42237  dvnprodlem1  42238  dvnprodlem2  42239  fourierdlem25  42424  fourierdlem37  42436  fourierdlem51  42449  fourierdlem79  42477  fouriersw  42523  etransclem16  42542  etransclem24  42550  etransclem33  42559  etransclem44  42570  sge0resplit  42695  sge0iunmptlemfi  42702  sge0iunmptlemre  42704  carageniuncllem2  42811  hsphoidmvle2  42874  hsphoidmvle  42875  hoidmvlelem4  42887  hoidmvlelem5  42888  fmtnoinf  43705  perfectALTVlem2  43894  rmsuppfi  44428  mndpsuppfi  44430  scmsuppfi  44432  suppmptcfin  44434