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		invdif	|- ( S i^i ( _V \ { Z } ) ) = ( S \ { Z } )
3	2	imaeq2i	|- ( `' F " ( S i^i ( _V \ { Z } ) ) ) = ( `' F " ( S \ { Z } ) )
4		ffun	|- ( F : I --> S -> Fun F )
5		inpreima	|- ( Fun F -> ( `' F " ( S i^i ( _V \ { Z } ) ) ) = ( ( `' F " S ) i^i ( `' F " ( _V \ { Z } ) ) ) )
6	4 5	syl	|- ( F : I --> S -> ( `' F " ( S i^i ( _V \ { Z } ) ) ) = ( ( `' F " S ) i^i ( `' F " ( _V \ { Z } ) ) ) )
7		cnvimass	|- ( `' F " ( _V \ { Z } ) ) C_ dom F
8		fdm	|- ( F : I --> S -> dom F = I )
9		fimacnv	|- ( F : I --> S -> ( `' F " S ) = I )
10	8 9	eqtr4d	|- ( F : I --> S -> dom F = ( `' F " S ) )
11	7 10	sseqtrid	|- ( F : I --> S -> ( `' F " ( _V \ { Z } ) ) C_ ( `' F " S ) )
12		sseqin2	|- ( ( `' F " ( _V \ { Z } ) ) C_ ( `' F " S ) <-> ( ( `' F " S ) i^i ( `' F " ( _V \ { Z } ) ) ) = ( `' F " ( _V \ { Z } ) ) )
13	11 12	sylib	|- ( F : I --> S -> ( ( `' F " S ) i^i ( `' F " ( _V \ { Z } ) ) ) = ( `' F " ( _V \ { Z } ) ) )
14	6 13	eqtrd	|- ( F : I --> S -> ( `' F " ( S i^i ( _V \ { Z } ) ) ) = ( `' F " ( _V \ { Z } ) ) )
15	3 14	syl5reqr	|- ( 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 } ) ) ) )