Theorem fofi 8419

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 8406	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴)
2		domfi 8348	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ Fin)
3	1, 2	syldan 488	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2139   class class class wbr 4804  –onto→wfo 6047   ≼ cdom 8121  Fincfn 8123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-om 7232  df-1o 7730  df-er 7913  df-en 8124  df-dom 8125  df-fin 8127

This theorem is referenced by:  f1fi  8420  imafi  8426  f1opwfi  8437  indexfi  8441  intrnfi  8489  infpwfien  9095  ttukeylem6  9548  fseqsupcl  12990  fiinfnf1o  13352  vdwlem6  15912  0ram2  15947  0ramcl  15949  mplsubrglem  19661  tgcmp  21426  hauscmplem  21431  1stcfb  21470  comppfsc  21557  1stckgenlem  21578  ptcnplem  21646  txtube  21665  txcmplem1  21666  tmdgsum2  22121  tsmsf1o  22169  tsmsxplem1  22177  ovolicc2lem4  23508  i1fadd  23681  i1fmul  23682  itg1addlem4  23685  i1fmulc  23689  mbfi1fseqlem4  23704  limciun  23877  edgusgrnbfin  26494  erdszelem2  31502  mvrsfpw  31731  itg2addnclem2  33793  istotbnd3  33901  sstotbnd  33905  prdsbnd  33923  cntotbnd  33926  heiborlem1  33941  heibor  33951  lmhmfgima  38174