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

Metamath Proof Explorer

Theorem fczfsuppd

Description: A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019)

Ref Expression
Hypotheses fczfsuppd.b 
|- ( ph -> B e. V )
fczfsuppd.z 
|- ( ph -> Z e. W )
Assertion fczfsuppd 
|- ( ph -> ( B X. { Z } ) finSupp Z )

Proof

Step Hyp Ref Expression
1 fczfsuppd.b 
 |-  ( ph -> B e. V )
2 fczfsuppd.z 
 |-  ( ph -> Z e. W )
3 fnconstg 
 |-  ( Z e. W -> ( B X. { Z } ) Fn B )
4 fnfun 
 |-  ( ( B X. { Z } ) Fn B -> Fun ( B X. { Z } ) )
5 2 3 4 3syl 
 |-  ( ph -> Fun ( B X. { Z } ) )
6 fczsupp0 
 |-  ( ( B X. { Z } ) supp Z ) = (/)
7 0fi 
 |-  (/) e. Fin
8 6 7 eqeltri 
 |-  ( ( B X. { Z } ) supp Z ) e. Fin
9 8 a1i 
 |-  ( ph -> ( ( B X. { Z } ) supp Z ) e. Fin )
10 snex 
 |-  { Z } e. _V
11 xpexg 
 |-  ( ( B e. V /\ { Z } e. _V ) -> ( B X. { Z } ) e. _V )
12 1 10 11 sylancl 
 |-  ( ph -> ( B X. { Z } ) e. _V )
13 isfsupp 
 |-  ( ( ( B X. { Z } ) e. _V /\ Z e. W ) -> ( ( B X. { Z } ) finSupp Z <-> ( Fun ( B X. { Z } ) /\ ( ( B X. { Z } ) supp Z ) e. Fin ) ) )
14 12 2 13 syl2anc 
 |-  ( ph -> ( ( B X. { Z } ) finSupp Z <-> ( Fun ( B X. { Z } ) /\ ( ( B X. { Z } ) supp Z ) e. Fin ) ) )
15 5 9 14 mpbir2and 
 |-  ( ph -> ( B X. { Z } ) finSupp Z )