MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fofi Structured version   Unicode version

Theorem fofi 7595
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  |-  ( ( A  e.  Fin  /\  F : A -onto-> B )  ->  B  e.  Fin )

Proof of Theorem fofi
StepHypRef Expression
1 fodomfi 7588 . 2  |-  ( ( A  e.  Fin  /\  F : A -onto-> B )  ->  B  ~<_  A )
2 domfi 7532 . 2  |-  ( ( A  e.  Fin  /\  B  ~<_  A )  ->  B  e.  Fin )
31, 2syldan 470 1  |-  ( ( A  e.  Fin  /\  F : A -onto-> B )  ->  B  e.  Fin )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   class class class wbr 4290   -onto->wfo 5414    ~<_ cdom 7306   Fincfn 7308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-sep 4411  ax-nul 4419  ax-pow 4468  ax-pr 4529  ax-un 6370
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3185  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-pss 3342  df-nul 3636  df-if 3790  df-pw 3860  df-sn 3876  df-pr 3878  df-tp 3880  df-op 3882  df-uni 4090  df-br 4291  df-opab 4349  df-tr 4384  df-eprel 4630  df-id 4634  df-po 4639  df-so 4640  df-fr 4677  df-we 4679  df-ord 4720  df-on 4721  df-lim 4722  df-suc 4723  df-xp 4844  df-rel 4845  df-cnv 4846  df-co 4847  df-dm 4848  df-rn 4849  df-res 4850  df-ima 4851  df-iota 5379  df-fun 5418  df-fn 5419  df-f 5420  df-f1 5421  df-fo 5422  df-f1o 5423  df-fv 5424  df-om 6475  df-1o 6918  df-er 7099  df-en 7309  df-dom 7310  df-fin 7312
This theorem is referenced by:  f1fi  7596  imafi  7602  f1opwfi  7613  indexfi  7617  intrnfi  7664  infpwfien  8230  ttukeylem6  8681  fseqsupcl  11797  fiinfnf1o  12119  vdwlem6  14045  0ram2  14080  0ramcl  14082  mplsubrglem  17515  mplsubrglemOLD  17516  tgcmp  19002  hauscmplem  19007  1stcfb  19047  1stckgenlem  19124  ptcnplem  19192  txtube  19211  txcmplem1  19212  tmdgsum2  19665  tsmsf1o  19717  tsmsxplem1  19725  ovolicc2lem4  21001  i1fadd  21171  i1fmul  21172  itg1addlem4  21175  i1fmulc  21179  mbfi1fseqlem4  21194  limciun  21367  edgusgranbfin  23356  erdszelem2  27078  itg2addnclem2  28441  comppfsc  28576  istotbnd3  28667  sstotbnd  28671  prdsbnd  28689  cntotbnd  28692  heiborlem1  28707  heibor  28717  lmhmfgima  29434
  Copyright terms: Public domain W3C validator