Theorem fofi 8802

Description: If a function has a finite domain, its range is finite. Theorem 37 of [Suppes] p. 104. (Contributed by NM, 25-Mar-2007.)

Assertion

Ref	Expression
fofi	⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ Fin)

Proof of Theorem fofi

Step	Hyp	Ref	Expression
1		fodomfi 8789	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴)
2		domfi 8731	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ Fin)
3	1, 2	syldan 593	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2108   class class class wbr 5057  –onto→wfo 6346   ≼ cdom 8499  Fincfn 8501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-om 7573  df-1o 8094  df-er 8281  df-en 8502  df-dom 8503  df-fin 8505

This theorem is referenced by:  f1fi  8803  imafi  8809  f1opwfi  8820  indexfi  8824  intrnfi  8872  infpwfien  9480  ttukeylem6  9928  fseqsupcl  13337  fiinfnf1o  13702  vdwlem6  16314  0ram2  16349  0ramcl  16351  mplsubrglem  20211  tgcmp  22001  hauscmplem  22006  1stcfb  22045  comppfsc  22132  1stckgenlem  22153  ptcnplem  22221  txtube  22240  txcmplem1  22241  tmdgsum2  22696  tsmsf1o  22745  tsmsxplem1  22753  ovolicc2lem4  24113  i1fadd  24288  i1fmul  24289  itg1addlem4  24292  i1fmulc  24296  mbfi1fseqlem4  24311  limciun  24484  edgusgrnbfin  27147  erdszelem2  32432  mvrsfpw  32746  itg2addnclem2  34936  istotbnd3  35041  sstotbnd  35045  prdsbnd  35063  cntotbnd  35066  heiborlem1  35081  heibor  35091  lmhmfgima  39674