Theorem fundcmpsurinjlem2

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

	Ref	Expression
Hypotheses	fundcmpsurinj.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
	fundcmpsurinj.g	|- G = ( x e. A |-> ( `' F " { ( F ` x ) } ) )
Assertion	fundcmpsurinjlem2	|- ( ( F Fn A /\ A e. V ) -> G : A -onto-> P )

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2		fundcmpsurinj.g	|- G = ( x e. A |-> ( `' F " { ( F ` x ) } ) )
3		fnex	|- ( ( F Fn A /\ A e. V ) -> F e. _V )
4		cnvexg	|- ( F e. _V -> `' F e. _V )
5		imaexg	|- ( `' F e. _V -> ( `' F " { ( F ` x ) } ) e. _V )
6	3 4 5	3syl	|- ( ( F Fn A /\ A e. V ) -> ( `' F " { ( F ` x ) } ) e. _V )
7	6	ralrimivw	|- ( ( F Fn A /\ A e. V ) -> A. x e. A ( `' F " { ( F ` x ) } ) e. _V )
8	2	fnmpt	|- ( A. x e. A ( `' F " { ( F ` x ) } ) e. _V -> G Fn A )
9	7 8	syl	|- ( ( F Fn A /\ A e. V ) -> G Fn A )
10	1 2	fundcmpsurinjlem1	|- ran G = P
11		df-fo	|- ( G : A -onto-> P <-> ( G Fn A /\ ran G = P ) )
12	9 10 11	sylanblrc	|- ( ( F Fn A /\ A e. V ) -> G : A -onto-> P )