Metamath Proof Explorer

Theorem imacosuppOLD

Description: Obsolete version of imacosupp as of 15-Sep-2023. The image of the support of the composition of two functions is the support of the outer function. (Contributed by AV, 30-May-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion imacosuppOLD 
|- ( ( F e. V /\ G e. W ) -> ( ( Fun G /\ ( F supp Z ) C_ ran G ) -> ( G " ( ( F o. G ) supp Z ) ) = ( F supp Z ) ) )

Proof

Step Hyp Ref Expression
1 cnvco 
 |-  `' ( F o. G ) = ( `' G o. `' F )
2 1 imaeq1i 
 |-  ( `' ( F o. G ) " ( _V \ { Z } ) ) = ( ( `' G o. `' F ) " ( _V \ { Z } ) )
3 imaco 
 |-  ( ( `' G o. `' F ) " ( _V \ { Z } ) ) = ( `' G " ( `' F " ( _V \ { Z } ) ) )
4 2 3 eqtri 
 |-  ( `' ( F o. G ) " ( _V \ { Z } ) ) = ( `' G " ( `' F " ( _V \ { Z } ) ) )
5 4 imaeq2i 
 |-  ( G " ( `' ( F o. G ) " ( _V \ { Z } ) ) ) = ( G " ( `' G " ( `' F " ( _V \ { Z } ) ) ) )
6 funforn 
 |-  ( Fun G <-> G : dom G -onto-> ran G )
7 6 biimpi 
 |-  ( Fun G -> G : dom G -onto-> ran G )
8 7 ad2antrl 
 |-  ( ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) /\ ( Fun G /\ ( F supp Z ) C_ ran G ) ) -> G : dom G -onto-> ran G )
9 simpl 
 |-  ( ( F e. V /\ G e. W ) -> F e. V )
10 9 anim2i 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( Z e. _V /\ F e. V ) )
11 10 ancomd 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( F e. V /\ Z e. _V ) )
12 suppimacnv 
 |-  ( ( F e. V /\ Z e. _V ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
13 11 12 syl 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
14 13 sseq1d 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( ( F supp Z ) C_ ran G <-> ( `' F " ( _V \ { Z } ) ) C_ ran G ) )
15 14 biimpd 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( ( F supp Z ) C_ ran G -> ( `' F " ( _V \ { Z } ) ) C_ ran G ) )
16 15 adantld 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( ( Fun G /\ ( F supp Z ) C_ ran G ) -> ( `' F " ( _V \ { Z } ) ) C_ ran G ) )
17 16 imp 
 |-  ( ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) /\ ( Fun G /\ ( F supp Z ) C_ ran G ) ) -> ( `' F " ( _V \ { Z } ) ) C_ ran G )
18 foimacnv 
 |-  ( ( G : dom G -onto-> ran G /\ ( `' F " ( _V \ { Z } ) ) C_ ran G ) -> ( G " ( `' G " ( `' F " ( _V \ { Z } ) ) ) ) = ( `' F " ( _V \ { Z } ) ) )
19 8 17 18 syl2anc 
 |-  ( ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) /\ ( Fun G /\ ( F supp Z ) C_ ran G ) ) -> ( G " ( `' G " ( `' F " ( _V \ { Z } ) ) ) ) = ( `' F " ( _V \ { Z } ) ) )
20 5 19 syl5eq 
 |-  ( ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) /\ ( Fun G /\ ( F supp Z ) C_ ran G ) ) -> ( G " ( `' ( F o. G ) " ( _V \ { Z } ) ) ) = ( `' F " ( _V \ { Z } ) ) )
21 coexg 
 |-  ( ( F e. V /\ G e. W ) -> ( F o. G ) e. _V )
22 21 anim2i 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( Z e. _V /\ ( F o. G ) e. _V ) )
23 22 ancomd 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( ( F o. G ) e. _V /\ Z e. _V ) )
24 suppimacnv 
 |-  ( ( ( F o. G ) e. _V /\ Z e. _V ) -> ( ( F o. G ) supp Z ) = ( `' ( F o. G ) " ( _V \ { Z } ) ) )
25 23 24 syl 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( ( F o. G ) supp Z ) = ( `' ( F o. G ) " ( _V \ { Z } ) ) )
26 25 imaeq2d 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( G " ( ( F o. G ) supp Z ) ) = ( G " ( `' ( F o. G ) " ( _V \ { Z } ) ) ) )
27 26 adantr 
 |-  ( ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) /\ ( Fun G /\ ( F supp Z ) C_ ran G ) ) -> ( G " ( ( F o. G ) supp Z ) ) = ( G " ( `' ( F o. G ) " ( _V \ { Z } ) ) ) )
28 13 adantr 
 |-  ( ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) /\ ( Fun G /\ ( F supp Z ) C_ ran G ) ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
29 20 27 28 3eqtr4d 
 |-  ( ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) /\ ( Fun G /\ ( F supp Z ) C_ ran G ) ) -> ( G " ( ( F o. G ) supp Z ) ) = ( F supp Z ) )
30 29 exp31 
 |-  ( Z e. _V -> ( ( F e. V /\ G e. W ) -> ( ( Fun G /\ ( F supp Z ) C_ ran G ) -> ( G " ( ( F o. G ) supp Z ) ) = ( F supp Z ) ) ) )
31 ima0 
 |-  ( G " (/) ) = (/)
32 id 
 |-  ( -. Z e. _V -> -. Z e. _V )
33 32 intnand 
 |-  ( -. Z e. _V -> -. ( ( F o. G ) e. _V /\ Z e. _V ) )
34 supp0prc 
 |-  ( -. ( ( F o. G ) e. _V /\ Z e. _V ) -> ( ( F o. G ) supp Z ) = (/) )
35 33 34 syl 
 |-  ( -. Z e. _V -> ( ( F o. G ) supp Z ) = (/) )
36 35 imaeq2d 
 |-  ( -. Z e. _V -> ( G " ( ( F o. G ) supp Z ) ) = ( G " (/) ) )
37 32 intnand 
 |-  ( -. Z e. _V -> -. ( F e. _V /\ Z e. _V ) )
38 supp0prc 
 |-  ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) = (/) )
39 37 38 syl 
 |-  ( -. Z e. _V -> ( F supp Z ) = (/) )
40 31 36 39 3eqtr4a 
 |-  ( -. Z e. _V -> ( G " ( ( F o. G ) supp Z ) ) = ( F supp Z ) )
41 40 2a1d 
 |-  ( -. Z e. _V -> ( ( F e. V /\ G e. W ) -> ( ( Fun G /\ ( F supp Z ) C_ ran G ) -> ( G " ( ( F o. G ) supp Z ) ) = ( F supp Z ) ) ) )
42 30 41 pm2.61i 
 |-  ( ( F e. V /\ G e. W ) -> ( ( Fun G /\ ( F supp Z ) C_ ran G ) -> ( G " ( ( F o. G ) supp Z ) ) = ( F supp Z ) ) )