Metamath Proof Explorer

Theorem fnsuppeq0

Description: The support of a function is empty iff it is identically zero. (Contributed by Stefan O'Rear, 22-Mar-2015) (Revised by AV, 28-May-2019)

Ref Expression
Assertion fnsuppeq0
`|- ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( ( F supp Z ) = (/) <-> F = ( A X. { Z } ) ) )`

Proof

Step Hyp Ref Expression
1 ss0b
` |-  ( ( F supp Z ) C_ (/) <-> ( F supp Z ) = (/) )`
2 un0
` |-  ( A u. (/) ) = A`
3 uncom
` |-  ( A u. (/) ) = ( (/) u. A )`
4 2 3 eqtr3i
` |-  A = ( (/) u. A )`
5 4 fneq2i
` |-  ( F Fn A <-> F Fn ( (/) u. A ) )`
6 5 biimpi
` |-  ( F Fn A -> F Fn ( (/) u. A ) )`
` |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> F Fn ( (/) u. A ) )`
8 fnex
` |-  ( ( F Fn A /\ A e. W ) -> F e. _V )`
` |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> F e. _V )`
10 simp3
` |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> Z e. V )`
11 0in
` |-  ( (/) i^i A ) = (/)`
12 11 a1i
` |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( (/) i^i A ) = (/) )`
13 fnsuppres
` |-  ( ( F Fn ( (/) u. A ) /\ ( F e. _V /\ Z e. V ) /\ ( (/) i^i A ) = (/) ) -> ( ( F supp Z ) C_ (/) <-> ( F |` A ) = ( A X. { Z } ) ) )`
14 7 9 10 12 13 syl121anc
` |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( ( F supp Z ) C_ (/) <-> ( F |` A ) = ( A X. { Z } ) ) )`
15 1 14 syl5bbr
` |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( ( F supp Z ) = (/) <-> ( F |` A ) = ( A X. { Z } ) ) )`
16 fnresdm
` |-  ( F Fn A -> ( F |` A ) = F )`
` |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( F |` A ) = F )`
` |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( ( F |` A ) = ( A X. { Z } ) <-> F = ( A X. { Z } ) ) )`
` |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( ( F supp Z ) = (/) <-> F = ( A X. { Z } ) ) )`