Theorem fundcmpsurinjlem3

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

	Ref	Expression
Hypotheses	fundcmpsurinj.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
	fundcmpsurinj.h	|- H = ( p e. P |-> U. ( F " p ) )
Assertion	fundcmpsurinjlem3	|- ( ( Fun F /\ X e. P ) -> ( H ` X ) = U. ( F " X ) )

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2		fundcmpsurinj.h	|- H = ( p e. P |-> U. ( F " p ) )
3	2	a1i	|- ( ( Fun F /\ X e. P ) -> H = ( p e. P |-> U. ( F " p ) ) )
4		imaeq2	|- ( p = X -> ( F " p ) = ( F " X ) )
5	4	unieqd	|- ( p = X -> U. ( F " p ) = U. ( F " X ) )
6	5	adantl	|- ( ( ( Fun F /\ X e. P ) /\ p = X ) -> U. ( F " p ) = U. ( F " X ) )
7		simpr	|- ( ( Fun F /\ X e. P ) -> X e. P )
8		funimaexg	|- ( ( Fun F /\ X e. P ) -> ( F " X ) e. _V )
9	8	uniexd	|- ( ( Fun F /\ X e. P ) -> U. ( F " X ) e. _V )
10	3 6 7 9	fvmptd	|- ( ( Fun F /\ X e. P ) -> ( H ` X ) = U. ( F " X ) )