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

Metamath Proof Explorer

Theorem fsuppeqg

Description: Version of fsuppeq avoiding ax-rep by assuming F is a set rather than its domain I . (Contributed by SN, 30-Jul-2024)

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

Proof

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