Theorem fczfsuppd

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

	Ref	Expression
Hypotheses	fczfsuppd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	fczfsuppd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
Assertion	fczfsuppd	⊢ ( 𝜑 → ( 𝐵 × { 𝑍 } ) finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		fczfsuppd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2		fczfsuppd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
3		snex	⊢ { 𝑍 } ∈ V
4		xpexg	⊢ ( ( 𝐵 ∈ 𝑉 ∧ { 𝑍 } ∈ V ) → ( 𝐵 × { 𝑍 } ) ∈ V )
5	1 3 4	sylancl	⊢ ( 𝜑 → ( 𝐵 × { 𝑍 } ) ∈ V )
6		fnconstg	⊢ ( 𝑍 ∈ 𝑊 → ( 𝐵 × { 𝑍 } ) Fn 𝐵 )
7		fnfun	⊢ ( ( 𝐵 × { 𝑍 } ) Fn 𝐵 → Fun ( 𝐵 × { 𝑍 } ) )
8	2 6 7	3syl	⊢ ( 𝜑 → Fun ( 𝐵 × { 𝑍 } ) )
9		fczsupp0	⊢ ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) = ∅
10		0fi	⊢ ∅ ∈ Fin
11	9 10	eqeltri	⊢ ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) ∈ Fin
12	11	a1i	⊢ ( 𝜑 → ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) ∈ Fin )
13	5 2 8 12	isfsuppd	⊢ ( 𝜑 → ( 𝐵 × { 𝑍 } ) finSupp 𝑍 )