This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsuppeq

Description: Two ways of writing the support of a function with known codomain. (Contributed by Stefan O'Rear, 9-Jul-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Assertion fsuppeq 
|- ( ( I e. V /\ Z e. W ) -> ( F : I --> S -> ( F supp Z ) = ( `' F " ( S \ { Z } ) ) ) )

Proof

Step Hyp Ref Expression
1 fex 
 |-  ( ( F : I --> S /\ I e. V ) -> F e. _V )
2 1 expcom 
 |-  ( I e. V -> ( F : I --> S -> F e. _V ) )
3 2 adantr 
 |-  ( ( I e. V /\ Z e. W ) -> ( F : I --> S -> F e. _V ) )
4 3 imp 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> F e. _V )
5 simplr 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> Z e. W )
6 suppimacnv 
 |-  ( ( F e. _V /\ Z e. W ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
7 4 5 6 syl2anc 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
8 ffun 
 |-  ( F : I --> S -> Fun F )
9 inpreima 
 |-  ( Fun F -> ( `' F " ( S i^i ( _V \ { Z } ) ) ) = ( ( `' F " S ) i^i ( `' F " ( _V \ { Z } ) ) ) )
10 8 9 syl 
 |-  ( F : I --> S -> ( `' F " ( S i^i ( _V \ { Z } ) ) ) = ( ( `' F " S ) i^i ( `' F " ( _V \ { Z } ) ) ) )
11 cnvimass 
 |-  ( `' F " ( _V \ { Z } ) ) C_ dom F
12 fdm 
 |-  ( F : I --> S -> dom F = I )
13 fimacnv 
 |-  ( F : I --> S -> ( `' F " S ) = I )
14 12 13 eqtr4d 
 |-  ( F : I --> S -> dom F = ( `' F " S ) )
15 11 14 sseqtrid 
 |-  ( F : I --> S -> ( `' F " ( _V \ { Z } ) ) C_ ( `' F " S ) )
16 sseqin2 
 |-  ( ( `' F " ( _V \ { Z } ) ) C_ ( `' F " S ) <-> ( ( `' F " S ) i^i ( `' F " ( _V \ { Z } ) ) ) = ( `' F " ( _V \ { Z } ) ) )
17 15 16 sylib 
 |-  ( F : I --> S -> ( ( `' F " S ) i^i ( `' F " ( _V \ { Z } ) ) ) = ( `' F " ( _V \ { Z } ) ) )
18 10 17 eqtrd 
 |-  ( F : I --> S -> ( `' F " ( S i^i ( _V \ { Z } ) ) ) = ( `' F " ( _V \ { Z } ) ) )
19 invdif 
 |-  ( S i^i ( _V \ { Z } ) ) = ( S \ { Z } )
20 19 imaeq2i 
 |-  ( `' F " ( S i^i ( _V \ { Z } ) ) ) = ( `' F " ( S \ { Z } ) )
21 18 20 eqtr3di 
 |-  ( F : I --> S -> ( `' F " ( _V \ { Z } ) ) = ( `' F " ( S \ { Z } ) ) )
22 21 adantl 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> ( `' F " ( _V \ { Z } ) ) = ( `' F " ( S \ { Z } ) ) )
23 7 22 eqtrd 
 |-  ( ( ( I e. V /\ Z e. W ) /\ F : I --> S ) -> ( F supp Z ) = ( `' F " ( S \ { Z } ) ) )
24 23 ex 
 |-  ( ( I e. V /\ Z e. W ) -> ( F : I --> S -> ( F supp Z ) = ( `' F " ( S \ { Z } ) ) ) )