Metamath Proof Explorer


Theorem fundcmpsurinjlem3

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

Ref Expression
Hypotheses fundcmpsurinj.p P=z|xAz=F-1Fx
fundcmpsurinj.h H=pPFp
Assertion fundcmpsurinjlem3 FunFXPHX=FX

Proof

Step Hyp Ref Expression
1 fundcmpsurinj.p P=z|xAz=F-1Fx
2 fundcmpsurinj.h H=pPFp
3 2 a1i FunFXPH=pPFp
4 imaeq2 p=XFp=FX
5 4 unieqd p=XFp=FX
6 5 adantl FunFXPp=XFp=FX
7 simpr FunFXPXP
8 funimaexg FunFXPFXV
9 8 uniexd FunFXPFXV
10 3 6 7 9 fvmptd FunFXPHX=FX