Metamath Proof Explorer


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 FVZWF:ISFsuppZ=F-1SZ

Proof

Step Hyp Ref Expression
1 suppimacnv FVZWFsuppZ=F-1VZ
2 ffun F:ISFunF
3 inpreima FunFF-1SVZ=F-1SF-1VZ
4 2 3 syl F:ISF-1SVZ=F-1SF-1VZ
5 cnvimass F-1VZdomF
6 fdm F:ISdomF=I
7 fimacnv F:ISF-1S=I
8 6 7 eqtr4d F:ISdomF=F-1S
9 5 8 sseqtrid F:ISF-1VZF-1S
10 sseqin2 F-1VZF-1SF-1SF-1VZ=F-1VZ
11 9 10 sylib F:ISF-1SF-1VZ=F-1VZ
12 4 11 eqtrd F:ISF-1SVZ=F-1VZ
13 invdif SVZ=SZ
14 13 imaeq2i F-1SVZ=F-1SZ
15 12 14 eqtr3di F:ISF-1VZ=F-1SZ
16 1 15 sylan9eq FVZWF:ISFsuppZ=F-1SZ
17 16 ex FVZWF:ISFsuppZ=F-1SZ