Metamath Proof Explorer


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 𝑍 ) = ∅