This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fidmfisupp

Description: A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses fidmfisupp.1 
|- ( ph -> F : D --> R )
fidmfisupp.2 
|- ( ph -> D e. Fin )
fidmfisupp.3 
|- ( ph -> Z e. V )
Assertion fidmfisupp 
|- ( ph -> F finSupp Z )

Proof

Step Hyp Ref Expression
1 fidmfisupp.1 
 |-  ( ph -> F : D --> R )
2 fidmfisupp.2 
 |-  ( ph -> D e. Fin )
3 fidmfisupp.3 
 |-  ( ph -> Z e. V )
4 1 2 fexd 
 |-  ( ph -> F e. _V )
5 suppimacnv 
 |-  ( ( F e. _V /\ Z e. V ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
6 4 3 5 syl2anc 
 |-  ( ph -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
7 2 1 fisuppfi 
 |-  ( ph -> ( `' F " ( _V \ { Z } ) ) e. Fin )
8 6 7 eqeltrd 
 |-  ( ph -> ( F supp Z ) e. Fin )
9 1 ffund 
 |-  ( ph -> Fun F )
10 funisfsupp 
 |-  ( ( Fun F /\ F e. _V /\ Z e. V ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
11 9 4 3 10 syl3anc 
 |-  ( ph -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
12 8 11 mpbird 
 |-  ( ph -> F finSupp Z )