Metamath Proof Explorer


Theorem fundcmpsurinjlem2

Description: Lemma 2 for fundcmpsurinj . (Contributed by AV, 4-Mar-2024)

Ref Expression
Hypotheses fundcmpsurinj.p P=z|xAz=F-1Fx
fundcmpsurinj.g G=xAF-1Fx
Assertion fundcmpsurinjlem2 FFnAAVG:AontoP

Proof

Step Hyp Ref Expression
1 fundcmpsurinj.p P=z|xAz=F-1Fx
2 fundcmpsurinj.g G=xAF-1Fx
3 fnex FFnAAVFV
4 cnvexg FVF-1V
5 imaexg F-1VF-1FxV
6 3 4 5 3syl FFnAAVF-1FxV
7 6 ralrimivw FFnAAVxAF-1FxV
8 2 fnmpt xAF-1FxVGFnA
9 7 8 syl FFnAAVGFnA
10 1 2 fundcmpsurinjlem1 ranG=P
11 df-fo G:AontoPGFnAranG=P
12 9 10 11 sylanblrc FFnAAVG:AontoP