Theorem fczsupp0

Description: The support of a constant function with value zero is empty. (Contributed by AV, 30-Jun-2019)

	Ref	Expression
Assertion	fczsupp0	⊢ ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		eqidd	⊢ ( ( ( 𝐵 × { 𝑍 } ) ∈ V ∧ 𝑍 ∈ V ) → ( 𝐵 × { 𝑍 } ) = ( 𝐵 × { 𝑍 } ) )
2		fnconstg	⊢ ( 𝑍 ∈ V → ( 𝐵 × { 𝑍 } ) Fn 𝐵 )
3	2	adantl	⊢ ( ( ( 𝐵 × { 𝑍 } ) ∈ V ∧ 𝑍 ∈ V ) → ( 𝐵 × { 𝑍 } ) Fn 𝐵 )
4		snnzg	⊢ ( 𝑍 ∈ V → { 𝑍 } ≠ ∅ )
5		simpl	⊢ ( ( ( 𝐵 × { 𝑍 } ) ∈ V ∧ 𝑍 ∈ V ) → ( 𝐵 × { 𝑍 } ) ∈ V )
6		xpexcnv	⊢ ( ( { 𝑍 } ≠ ∅ ∧ ( 𝐵 × { 𝑍 } ) ∈ V ) → 𝐵 ∈ V )
7	4 5 6	syl2an2	⊢ ( ( ( 𝐵 × { 𝑍 } ) ∈ V ∧ 𝑍 ∈ V ) → 𝐵 ∈ V )
8		simpr	⊢ ( ( ( 𝐵 × { 𝑍 } ) ∈ V ∧ 𝑍 ∈ V ) → 𝑍 ∈ V )
9		fnsuppeq0	⊢ ( ( ( 𝐵 × { 𝑍 } ) Fn 𝐵 ∧ 𝐵 ∈ V ∧ 𝑍 ∈ V ) → ( ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) = ∅ ↔ ( 𝐵 × { 𝑍 } ) = ( 𝐵 × { 𝑍 } ) ) )
10	3 7 8 9	syl3anc	⊢ ( ( ( 𝐵 × { 𝑍 } ) ∈ V ∧ 𝑍 ∈ V ) → ( ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) = ∅ ↔ ( 𝐵 × { 𝑍 } ) = ( 𝐵 × { 𝑍 } ) ) )
11	1 10	mpbird	⊢ ( ( ( 𝐵 × { 𝑍 } ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) = ∅ )
12		supp0prc	⊢ ( ¬ ( ( 𝐵 × { 𝑍 } ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) = ∅ )
13	11 12	pm2.61i	⊢ ( ( 𝐵 × { 𝑍 } ) supp 𝑍 ) = ∅