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=\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}$$
	fundcmpsurinj.h	$$⊢H=\left(p\in P⟼\bigcup F\left[p\right]\right)$$
Assertion	imasetpreimafvbijlemf	$$⊢FFnA\to H:P⟶F\left[A\right]$$

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	$$⊢P=\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}$$
2		fundcmpsurinj.h	$$⊢H=\left(p\in P⟼\bigcup F\left[p\right]\right)$$
3	1	uniimaelsetpreimafv	$$⊢\left(FFnA\wedge p\in P\right)\to \bigcup F\left[p\right]\in \mathrm{ran}F$$
4		fnima	$$⊢FFnA\to F\left[A\right]=\mathrm{ran}F$$
5	4	adantr	$$⊢\left(FFnA\wedge p\in P\right)\to F\left[A\right]=\mathrm{ran}F$$
6	3 5	eleqtrrd	$$⊢\left(FFnA\wedge p\in P\right)\to \bigcup F\left[p\right]\in F\left[A\right]$$
7	6 2	fmptd	$$⊢FFnA\to H:P⟶F\left[A\right]$$