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

Theorem fisuppfi 14499
Description: A function on a finite set is finitely supported. (Contributed by Mario Carneiro, 20-Jun-2015.)
Hypotheses
Ref Expression
fisuppfi.1  |-  ( ph  ->  A  e.  Fin )
fisuppfi.2  |-  ( ph  ->  F : A --> B )
Assertion
Ref Expression
fisuppfi  |-  ( ph  ->  ( `' F " C )  e.  Fin )

Proof of Theorem fisuppfi
StepHypRef Expression
1 fisuppfi.1 . 2  |-  ( ph  ->  A  e.  Fin )
2 cnvimass 5070 . . 3  |-  ( `' F " C ) 
C_  dom  F
3 fisuppfi.2 . . . 4  |-  ( ph  ->  F : A --> B )
4 fdm 5431 . . . 4  |-  ( F : A --> B  ->  dom  F  =  A )
53, 4syl 15 . . 3  |-  ( ph  ->  dom  F  =  A )
62, 5syl5sseq 3260 . 2  |-  ( ph  ->  ( `' F " C )  C_  A
)
7 ssfi 7126 . 2  |-  ( ( A  e.  Fin  /\  ( `' F " C ) 
C_  A )  -> 
( `' F " C )  e.  Fin )
81, 6, 7syl2anc 642 1  |-  ( ph  ->  ( `' F " C )  e.  Fin )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1633    e. wcel 1701    C_ wss 3186   `'ccnv 4725   dom cdm 4726   "cima 4729   -->wf 5288   Fincfn 6906
This theorem is referenced by:  psrmulcllem  16181  psrass1  16199  tmdgsum  17830  tsmslem1  17863  tsmssubm  17877  tsmsres  17878  tsmsf1o  17879  tsmsmhm  17880  tsmsadd  17881  tsmsxplem1  17887  tsmsxplem2  17888  imasdsf1olem  17989  xrge0gsumle  18390  xrge0tsms  18391  plypf1  19647  taylpfval  19797  jensenlem2  20335  jensen  20336  amgmlem  20337  amgm  20338  wilthlem2  20360  wilthlem3  20361  lgseisenlem3  20643  xrge0tsmsd  23360  gsumesum  23627  esumlub  23628  esumpfinval  23641  esumpfinvalf  23642  fprodss  24451  elfilspd  26403  mamucl  26604  mamuass  26608  mamudi  26609  mamudir  26610  mamuvs1  26611  mamuvs2  26612  matbas2  26623
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-er 6702  df-en 6907  df-fin 6910
  Copyright terms: Public domain W3C validator