Theorem fofi 9283

Description: If an onto function has a finite domain, its codomain/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 9282	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴)
2		domfi 9183	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ Fin)
3	1, 2	syldan 603	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ Fin)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   class class class wbr 5114  –onto→wfo 6541   ≼ cdom 8950  Fincfn 8952

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-om 7872  df-1o 8462  df-en 8953  df-dom 8954  df-fin 8956

This theorem is used by:  f1fi  9284  imafi  9285  f1opwfi  9323  indexfi  9327  intrnfi  9386  infpwfien  10065  ttukeylem6  10516  fseqsupcl  14033  fiinfnf1o  14406  vdwlem6  17071  0ram2  17106  0ramcl  17108  mplsubrglem  22190  tgcmp  23595  hauscmplem  23600  1stcfb  23639  comppfsc  23726  1stckgenlem  23747  ptcnplem  23815  txtube  23834  txcmplem1  23835  tmdgsum2  24290  tsmsf1o  24339  tsmsxplem1  24347  ovolicc2lem4  25716  i1fadd  25891  i1fmul  25892  itg1addlem4  25895  i1fmulc  25899  mbfi1fseqlem4  25914  limciun  26090  edgusgrnbfin  29760  fsupprnfi  33074  erdszelem2  35705  mvrsfpw  36019  itg2addnclem2  38364  istotbnd3  38463  sstotbnd  38467  prdsbnd  38485  cntotbnd  38488  heiborlem1  38503  heibor  38513  lmhmfgima  43852