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 
|- ( ( B X. { Z } ) supp Z ) = (/)

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( ( ( B X. { Z } ) e. _V /\ Z e. _V ) -> ( B X. { Z } ) = ( B X. { Z } ) )
2 fnconstg 
 |-  ( Z e. _V -> ( B X. { Z } ) Fn B )
3 2 adantl 
 |-  ( ( ( B X. { Z } ) e. _V /\ Z e. _V ) -> ( B X. { Z } ) Fn B )
4 snnzg 
 |-  ( Z e. _V -> { Z } =/= (/) )
5 simpl 
 |-  ( ( ( B X. { Z } ) e. _V /\ Z e. _V ) -> ( B X. { Z } ) e. _V )
6 xpexcnv 
 |-  ( ( { Z } =/= (/) /\ ( B X. { Z } ) e. _V ) -> B e. _V )
7 4 5 6 syl2an2 
 |-  ( ( ( B X. { Z } ) e. _V /\ Z e. _V ) -> B e. _V )
8 simpr 
 |-  ( ( ( B X. { Z } ) e. _V /\ Z e. _V ) -> Z e. _V )
9 fnsuppeq0 
 |-  ( ( ( B X. { Z } ) Fn B /\ B e. _V /\ Z e. _V ) -> ( ( ( B X. { Z } ) supp Z ) = (/) <-> ( B X. { Z } ) = ( B X. { Z } ) ) )
10 3 7 8 9 syl3anc 
 |-  ( ( ( B X. { Z } ) e. _V /\ Z e. _V ) -> ( ( ( B X. { Z } ) supp Z ) = (/) <-> ( B X. { Z } ) = ( B X. { Z } ) ) )
11 1 10 mpbird 
 |-  ( ( ( B X. { Z } ) e. _V /\ Z e. _V ) -> ( ( B X. { Z } ) supp Z ) = (/) )
12 supp0prc 
 |-  ( -. ( ( B X. { Z } ) e. _V /\ Z e. _V ) -> ( ( B X. { Z } ) supp Z ) = (/) )
13 11 12 pm2.61i 
 |-  ( ( B X. { Z } ) supp Z ) = (/)