Metamath Proof Explorer

Theorem supppreima

Description: Express the support of a function as the preimage of its range except zero. (Contributed by Thierry Arnoux, 24-Jun-2024)

Ref Expression
Assertion supppreima 
|- ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F supp Z ) = ( `' F " ( ran F \ { Z } ) ) )

Proof

Step Hyp Ref Expression
1 cnvimarndm 
 |-  ( `' F " ran F ) = dom F
2 1 a1i 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( `' F " ran F ) = dom F )
3 2 difeq1d 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( ( `' F " ran F ) \ ( `' F " { Z } ) ) = ( dom F \ ( `' F " { Z } ) ) )
4 difpreima 
 |-  ( Fun F -> ( `' F " ( ran F \ { Z } ) ) = ( ( `' F " ran F ) \ ( `' F " { Z } ) ) )
5 4 3ad2ant1 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( `' F " ( ran F \ { Z } ) ) = ( ( `' F " ran F ) \ ( `' F " { Z } ) ) )
6 suppssdm 
 |-  ( F supp Z ) C_ dom F
7 dfss4 
 |-  ( ( F supp Z ) C_ dom F <-> ( dom F \ ( dom F \ ( F supp Z ) ) ) = ( F supp Z ) )
8 6 7 mpbi 
 |-  ( dom F \ ( dom F \ ( F supp Z ) ) ) = ( F supp Z )
9 suppiniseg 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( dom F \ ( F supp Z ) ) = ( `' F " { Z } ) )
10 9 difeq2d 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( dom F \ ( dom F \ ( F supp Z ) ) ) = ( dom F \ ( `' F " { Z } ) ) )
11 8 10 eqtr3id 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F supp Z ) = ( dom F \ ( `' F " { Z } ) ) )
12 3 5 11 3eqtr4rd 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F supp Z ) = ( `' F " ( ran F \ { Z } ) ) )