Theorem imasetpreimafvbijlemf

Description: Lemma for imasetpreimafvbij : the mapping H is a function into the range of function F . (Contributed by AV, 22-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	imasetpreimafvbijlemf	|- ( F Fn A -> H : P --> ( F " A ) )

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	1	uniimaelsetpreimafv	|- ( ( F Fn A /\ p e. P ) -> U. ( F " p ) e. ran F )
4		fnima	|- ( F Fn A -> ( F " A ) = ran F )
5	4	adantr	|- ( ( F Fn A /\ p e. P ) -> ( F " A ) = ran F )
6	3 5	eleqtrrd	|- ( ( F Fn A /\ p e. P ) -> U. ( F " p ) e. ( F " A ) )
7	6 2	fmptd	|- ( F Fn A -> H : P --> ( F " A ) )