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 disjdif 
 |-  ( ( F supp Z ) i^i ( dom F \ ( F supp Z ) ) ) = (/)
9 8 a1i 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( ( F supp Z ) i^i ( dom F \ ( F supp Z ) ) ) = (/) )
10 reldisjun 
 |-  ( ( Rel F /\ dom F = ( ( F supp Z ) u. ( dom F \ ( F supp Z ) ) ) /\ ( ( F supp Z ) i^i ( dom F \ ( F supp Z ) ) ) = (/) ) -> F = ( ( F |` ( F supp Z ) ) u. ( F |` ( dom F \ ( F supp Z ) ) ) ) )
11 2 7 9 10 syl3anc 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> F = ( ( F |` ( F supp Z ) ) u. ( F |` ( dom F \ ( F supp Z ) ) ) ) )
12 11 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 ) ) ) ) )
13 resss 
 |-  ( F |` ( dom F \ ( F supp Z ) ) ) C_ F
14 sseqin2 
 |-  ( ( F |` ( dom F \ ( F supp Z ) ) ) C_ F <-> ( F i^i ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F |` ( dom F \ ( F supp Z ) ) ) )
15 13 14 mpbi 
 |-  ( F i^i ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F |` ( dom F \ ( F supp Z ) ) )
16 suppiniseg 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( dom F \ ( F supp Z ) ) = ( `' F " { Z } ) )
17 16 reseq2d 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F |` ( dom F \ ( F supp Z ) ) ) = ( F |` ( `' F " { Z } ) ) )
18 cnvrescnv 
 |-  `' ( `' F |` { Z } ) = ( F i^i ( _V X. { Z } ) )
19 funcnvres2 
 |-  ( Fun F -> `' ( `' F |` { Z } ) = ( F |` ( `' F " { Z } ) ) )
20 18 19 eqtr3id 
 |-  ( Fun F -> ( F i^i ( _V X. { Z } ) ) = ( F |` ( `' F " { Z } ) ) )
21 20 3ad2ant1 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F i^i ( _V X. { Z } ) ) = ( F |` ( `' F " { Z } ) ) )
22 17 21 eqtr4d 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F |` ( dom F \ ( F supp Z ) ) ) = ( F i^i ( _V X. { Z } ) ) )
23 15 22 syl5eq 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F i^i ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F i^i ( _V X. { Z } ) ) )
24 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 } ) ) )
25 23 24 sylib 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F \ ( F |` ( dom F \ ( F supp Z ) ) ) ) = ( F \ ( _V X. { Z } ) ) )
26 8 reseq2i 
 |-  ( F |` ( ( F supp Z ) i^i ( dom F \ ( F supp Z ) ) ) ) = ( F |` (/) )
27 resindi 
 |-  ( F |` ( ( F supp Z ) i^i ( dom F \ ( F supp Z ) ) ) ) = ( ( F |` ( F supp Z ) ) i^i ( F |` ( dom F \ ( F supp Z ) ) ) )
28 res0 
 |-  ( F |` (/) ) = (/)
29 26 27 28 3eqtr3i 
 |-  ( ( F |` ( F supp Z ) ) i^i ( F |` ( dom F \ ( F supp Z ) ) ) ) = (/)
30 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 ) ) )
31 29 30 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 ) ) )
32 12 25 31 3eqtr3rd 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F |` ( F supp Z ) ) = ( F \ ( _V X. { Z } ) ) )