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		snex	|- { Z } e. _V
4		xpexg	|- ( ( B e. V /\ { Z } e. _V ) -> ( B X. { Z } ) e. _V )
5	1 3 4	sylancl	|- ( ph -> ( B X. { Z } ) e. _V )
6		fnconstg	|- ( Z e. W -> ( B X. { Z } ) Fn B )
7		fnfun	|- ( ( B X. { Z } ) Fn B -> Fun ( B X. { Z } ) )
8	2 6 7	3syl	|- ( ph -> Fun ( B X. { Z } ) )
9		fczsupp0	|- ( ( B X. { Z } ) supp Z ) = (/)
10		0fi	|- (/) e. Fin
11	9 10	eqeltri	|- ( ( B X. { Z } ) supp Z ) e. Fin
12	11	a1i	|- ( ph -> ( ( B X. { Z } ) supp Z ) e. Fin )
13	5 2 8 12	isfsuppd	|- ( ph -> ( B X. { Z } ) finSupp Z )