Metamath Proof Explorer

Theorem fressupp

Description: The restriction of a function to its support. (Contributed by Thierry Arnoux, 25-Jun-2024)

Ref Expression
Assertion fressupp 
|- ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F |` ( F supp Z ) ) = ( F \ ( _V X. { Z } ) ) )

Proof

Step Hyp Ref Expression
1 funrel 
 |-  ( Fun F -> Rel F )
2 1 3ad2ant1 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> Rel F )
3 suppssdm 
 |-  ( F supp Z ) C_ dom F
4 undif 
 |-  ( ( F supp Z ) C_ dom F <-> ( ( F supp Z ) u. ( dom F \ ( F supp Z ) ) ) = dom F )
5 4 biimpi 
 |-  ( ( F supp Z ) C_ dom F -> ( ( F supp Z ) u. ( dom F \ ( F supp Z ) ) ) = dom F )
6 5 eqcomd 
 |-  ( ( F supp Z ) C_ dom F -> dom F = ( ( F supp Z ) u. ( dom F \ ( F supp Z ) ) ) )
7 3 6 mp1i 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> dom F = ( ( F supp Z ) u. ( dom F \ ( F supp Z ) ) ) )
8 reldmun 
 |-  ( ( Rel F /\ dom F = ( ( F supp Z ) u. ( dom F \ ( F supp Z ) ) ) ) -> F = ( ( F |` ( F supp Z ) ) u. ( F |` ( dom F \ ( F supp Z ) ) ) ) )
9 2 7 8 syl2anc 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> F = ( ( F |` ( F supp Z ) ) u. ( F |` ( dom F \ ( F supp Z ) ) ) ) )
10 9 difeq1d 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F \ ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( ( ( F |` ( F supp Z ) ) u. ( F |` ( dom F \ ( F supp Z ) ) ) ) \ ( F |` ( dom F \ ( F supp Z ) ) ) ) )
11 resss 
 |-  ( F |` ( dom F \ ( F supp Z ) ) ) C_ F
12 sseqin2 
 |-  ( ( F |` ( dom F \ ( F supp Z ) ) ) C_ F <-> ( F i^i ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F |` ( dom F \ ( F supp Z ) ) ) )
13 11 12 mpbi 
 |-  ( F i^i ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F |` ( dom F \ ( F supp Z ) ) )
14 suppiniseg 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( dom F \ ( F supp Z ) ) = ( `' F " { Z } ) )
15 14 reseq2d 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F |` ( dom F \ ( F supp Z ) ) ) = ( F |` ( `' F " { Z } ) ) )
16 cnvrescnv 
 |-  `' ( `' F |` { Z } ) = ( F i^i ( _V X. { Z } ) )
17 funcnvres2 
 |-  ( Fun F -> `' ( `' F |` { Z } ) = ( F |` ( `' F " { Z } ) ) )
18 16 17 eqtr3id 
 |-  ( Fun F -> ( F i^i ( _V X. { Z } ) ) = ( F |` ( `' F " { Z } ) ) )
19 18 3ad2ant1 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F i^i ( _V X. { Z } ) ) = ( F |` ( `' F " { Z } ) ) )
20 15 19 eqtr4d 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F |` ( dom F \ ( F supp Z ) ) ) = ( F i^i ( _V X. { Z } ) ) )
21 13 20 eqtrid 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F i^i ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F i^i ( _V X. { Z } ) ) )
22 indifbi 
 |-  ( ( F i^i ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F i^i ( _V X. { Z } ) ) <-> ( F \ ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F \ ( _V X. { Z } ) ) )
23 21 22 sylib 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F \ ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F \ ( _V X. { Z } ) ) )
24 disjdif 
 |-  ( ( F supp Z ) i^i ( dom F \ ( F supp Z ) ) ) = (/)
25 24 reseq2i 
 |-  ( F |` ( ( F supp Z ) i^i ( dom F \ ( F supp Z ) ) ) ) = ( F |` (/) )
26 resindi 
 |-  ( F |` ( ( F supp Z ) i^i ( dom F \ ( F supp Z ) ) ) ) = ( ( F |` ( F supp Z ) ) i^i ( F |` ( dom F \ ( F supp Z ) ) ) )
27 res0 
 |-  ( F |` (/) ) = (/)
28 25 26 27 3eqtr3i 
 |-  ( ( F |` ( F supp Z ) ) i^i ( F |` ( dom F \ ( F supp Z ) ) ) ) = (/)
29 undif5 
 |-  ( ( ( F |` ( F supp Z ) ) i^i ( F |` ( dom F \ ( F supp Z ) ) ) ) = (/) -> ( ( ( F |` ( F supp Z ) ) u. ( F |` ( dom F \ ( F supp Z ) ) ) ) \ ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F |` ( F supp Z ) ) )
30 28 29 mp1i 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( ( ( F |` ( F supp Z ) ) u. ( F |` ( dom F \ ( F supp Z ) ) ) ) \ ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F |` ( F supp Z ) ) )
31 10 23 30 3eqtr3rd 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F |` ( F supp Z ) ) = ( F \ ( _V X. { Z } ) ) )