Theorem frnsuppeqg

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

	Ref	Expression
Assertion	frnsuppeqg	|- ( ( 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 } ) ) ) )