Theorem imasetpreimafvbijlemfo

Description: Lemma for imasetpreimafvbij : the mapping H is a function onto 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	imasetpreimafvbijlemfo	$$⊢\left(FFnA\wedge A\in V\right)\to H:P\underset{onto}{⟶}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 2	imasetpreimafvbijlemf	$$⊢FFnA\to H:P⟶F\left[A\right]$$
4	3	adantr	$$⊢\left(FFnA\wedge A\in V\right)\to H:P⟶F\left[A\right]$$
5	1	preimafvelsetpreimafv	$$⊢\left(FFnA\wedge A\in V\wedge a\in A\right)\to F^{-1}\left[\left\{F\left(a\right)\right\}\right]\in P$$
6	5	3expa	$$⊢\left(\left(FFnA\wedge A\in V\right)\wedge a\in A\right)\to F^{-1}\left[\left\{F\left(a\right)\right\}\right]\in P$$
7		imaeq2	$$⊢p=F^{-1}\left[\left\{F\left(a\right)\right\}\right]\to F\left[p\right]=F\left[F^{-1}\left[\left\{F\left(a\right)\right\}\right]\right]$$
8	7	unieqd	$$⊢p=F^{-1}\left[\left\{F\left(a\right)\right\}\right]\to \bigcup F\left[p\right]=\bigcup F\left[F^{-1}\left[\left\{F\left(a\right)\right\}\right]\right]$$
9	8	eqeq2d	$$⊢p=F^{-1}\left[\left\{F\left(a\right)\right\}\right]\to \left(F\left(a\right)=\bigcup F\left[p\right]\leftrightarrow F\left(a\right)=\bigcup F\left[F^{-1}\left[\left\{F\left(a\right)\right\}\right]\right]\right)$$
10	9	adantl	$$⊢\left(\left(\left(FFnA\wedge A\in V\right)\wedge a\in A\right)\wedge p=F^{-1}\left[\left\{F\left(a\right)\right\}\right]\right)\to \left(F\left(a\right)=\bigcup F\left[p\right]\leftrightarrow F\left(a\right)=\bigcup F\left[F^{-1}\left[\left\{F\left(a\right)\right\}\right]\right]\right)$$
11		uniimaprimaeqfv	$$⊢\left(FFnA\wedge a\in A\right)\to \bigcup F\left[F^{-1}\left[\left\{F\left(a\right)\right\}\right]\right]=F\left(a\right)$$
12	11	adantlr	$$⊢\left(\left(FFnA\wedge A\in V\right)\wedge a\in A\right)\to \bigcup F\left[F^{-1}\left[\left\{F\left(a\right)\right\}\right]\right]=F\left(a\right)$$
13	12	eqcomd	$$⊢\left(\left(FFnA\wedge A\in V\right)\wedge a\in A\right)\to F\left(a\right)=\bigcup F\left[F^{-1}\left[\left\{F\left(a\right)\right\}\right]\right]$$
14	6 10 13	rspcedvd	$$⊢\left(\left(FFnA\wedge A\in V\right)\wedge a\in A\right)\to \exists p\in PF\left(a\right)=\bigcup F\left[p\right]$$
15		eqeq1	$$⊢y=F\left(a\right)\to \left(y=\bigcup F\left[p\right]\leftrightarrow F\left(a\right)=\bigcup F\left[p\right]\right)$$
16	15	eqcoms	$$⊢F\left(a\right)=y\to \left(y=\bigcup F\left[p\right]\leftrightarrow F\left(a\right)=\bigcup F\left[p\right]\right)$$
17	16	rexbidv	$$⊢F\left(a\right)=y\to \left(\exists p\in Py=\bigcup F\left[p\right]\leftrightarrow \exists p\in PF\left(a\right)=\bigcup F\left[p\right]\right)$$
18	14 17	syl5ibrcom	$$⊢\left(\left(FFnA\wedge A\in V\right)\wedge a\in A\right)\to \left(F\left(a\right)=y\to \exists p\in Py=\bigcup F\left[p\right]\right)$$
19	18	rexlimdva	$$⊢\left(FFnA\wedge A\in V\right)\to \left(\exists a\in AF\left(a\right)=y\to \exists p\in Py=\bigcup F\left[p\right]\right)$$
20	8	eqcomd	$$⊢p=F^{-1}\left[\left\{F\left(a\right)\right\}\right]\to \bigcup F\left[F^{-1}\left[\left\{F\left(a\right)\right\}\right]\right]=\bigcup F\left[p\right]$$
21	13 20	sylan9eq	$$⊢\left(\left(\left(FFnA\wedge A\in V\right)\wedge a\in A\right)\wedge p=F^{-1}\left[\left\{F\left(a\right)\right\}\right]\right)\to F\left(a\right)=\bigcup F\left[p\right]$$
22	21	ex	$$⊢\left(\left(FFnA\wedge A\in V\right)\wedge a\in A\right)\to \left(p=F^{-1}\left[\left\{F\left(a\right)\right\}\right]\to F\left(a\right)=\bigcup F\left[p\right]\right)$$
23	22	reximdva	$$⊢\left(FFnA\wedge A\in V\right)\to \left(\exists a\in Ap=F^{-1}\left[\left\{F\left(a\right)\right\}\right]\to \exists a\in AF\left(a\right)=\bigcup F\left[p\right]\right)$$
24	1	elsetpreimafv	$$⊢p\in P\to \exists x\in Ap=F^{-1}\left[\left\{F\left(x\right)\right\}\right]$$
25		fveq2	$$⊢a=x\to F\left(a\right)=F\left(x\right)$$
26	25	sneqd	$$⊢a=x\to \left\{F\left(a\right)\right\}=\left\{F\left(x\right)\right\}$$
27	26	imaeq2d	$$⊢a=x\to F^{-1}\left[\left\{F\left(a\right)\right\}\right]=F^{-1}\left[\left\{F\left(x\right)\right\}\right]$$
28	27	eqeq2d	$$⊢a=x\to \left(p=F^{-1}\left[\left\{F\left(a\right)\right\}\right]\leftrightarrow p=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right)$$
29	28	cbvrexvw	$$⊢\exists a\in Ap=F^{-1}\left[\left\{F\left(a\right)\right\}\right]\leftrightarrow \exists x\in Ap=F^{-1}\left[\left\{F\left(x\right)\right\}\right]$$
30	24 29	sylibr	$$⊢p\in P\to \exists a\in Ap=F^{-1}\left[\left\{F\left(a\right)\right\}\right]$$
31	23 30	impel	$$⊢\left(\left(FFnA\wedge A\in V\right)\wedge p\in P\right)\to \exists a\in AF\left(a\right)=\bigcup F\left[p\right]$$
32		eqeq2	$$⊢y=\bigcup F\left[p\right]\to \left(F\left(a\right)=y\leftrightarrow F\left(a\right)=\bigcup F\left[p\right]\right)$$
33	32	rexbidv	$$⊢y=\bigcup F\left[p\right]\to \left(\exists a\in AF\left(a\right)=y\leftrightarrow \exists a\in AF\left(a\right)=\bigcup F\left[p\right]\right)$$
34	31 33	syl5ibrcom	$$⊢\left(\left(FFnA\wedge A\in V\right)\wedge p\in P\right)\to \left(y=\bigcup F\left[p\right]\to \exists a\in AF\left(a\right)=y\right)$$
35	34	rexlimdva	$$⊢\left(FFnA\wedge A\in V\right)\to \left(\exists p\in Py=\bigcup F\left[p\right]\to \exists a\in AF\left(a\right)=y\right)$$
36	19 35	impbid	$$⊢\left(FFnA\wedge A\in V\right)\to \left(\exists a\in AF\left(a\right)=y\leftrightarrow \exists p\in Py=\bigcup F\left[p\right]\right)$$
37	36	abbidv	$$⊢\left(FFnA\wedge A\in V\right)\to \left\{y|\exists a\in AF\left(a\right)=y\right\}=\left\{y|\exists p\in Py=\bigcup F\left[p\right]\right\}$$
38		fnfun	$$⊢FFnA\to \mathrm{Fun}F$$
39		fndm	$$⊢FFnA\to \mathrm{dom}F=A$$
40		eqimss2	$$⊢\mathrm{dom}F=A\to A\subseteq \mathrm{dom}F$$
41	39 40	syl	$$⊢FFnA\to A\subseteq \mathrm{dom}F$$
42	38 41	jca	$$⊢FFnA\to \left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)$$
43	42	adantr	$$⊢\left(FFnA\wedge A\in V\right)\to \left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)$$
44		dfimafn	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to F\left[A\right]=\left\{y|\exists a\in AF\left(a\right)=y\right\}$$
45	43 44	syl	$$⊢\left(FFnA\wedge A\in V\right)\to F\left[A\right]=\left\{y|\exists a\in AF\left(a\right)=y\right\}$$
46	2	rnmpt	$$⊢\mathrm{ran}H=\left\{y|\exists p\in Py=\bigcup F\left[p\right]\right\}$$
47	46	a1i	$$⊢\left(FFnA\wedge A\in V\right)\to \mathrm{ran}H=\left\{y|\exists p\in Py=\bigcup F\left[p\right]\right\}$$
48	37 45 47	3eqtr4rd	$$⊢\left(FFnA\wedge A\in V\right)\to \mathrm{ran}H=F\left[A\right]$$
49		dffo2	$$⊢H:P\underset{onto}{⟶}F\left[A\right]\leftrightarrow \left(H:P⟶F\left[A\right]\wedge \mathrm{ran}H=F\left[A\right]\right)$$
50	4 48 49	sylanbrc	$$⊢\left(FFnA\wedge A\in V\right)\to H:P\underset{onto}{⟶}F\left[A\right]$$