Theorem imasetpreimafvbij

Description: The mapping H is a bijective function between the set P of all preimages of values of function F and the range of 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	imasetpreimafvbij	$$⊢\left(FFnA\wedge A\in V\right)\to H:P\underset{1-1\; 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	imasetpreimafvbijlemf1	$$⊢FFnA\to H:P\underset{1-1}{⟶}F\left[A\right]$$
4	3	adantr	$$⊢\left(FFnA\wedge A\in V\right)\to H:P\underset{1-1}{⟶}F\left[A\right]$$
5	1 2	imasetpreimafvbijlemfo	$$⊢\left(FFnA\wedge A\in V\right)\to H:P\underset{onto}{⟶}F\left[A\right]$$
6		df-f1o	$$⊢H:P\underset{1-1\; onto}{⟶}F\left[A\right]\leftrightarrow \left(H:P\underset{1-1}{⟶}F\left[A\right]\wedge H:P\underset{onto}{⟶}F\left[A\right]\right)$$
7	4 5 6	sylanbrc	$$⊢\left(FFnA\wedge A\in V\right)\to H:P\underset{1-1\; onto}{⟶}F\left[A\right]$$