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		0fin	|- (/) 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 )