Theorem fundcmpsurinjlem3

Description: Lemma 3 for fundcmpsurinj . (Contributed by AV, 3-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	fundcmpsurinjlem3	$$⊢\left(\mathrm{Fun}F\wedge X\in P\right)\to H\left(X\right)=\bigcup F\left[X\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	2	a1i	$$⊢\left(\mathrm{Fun}F\wedge X\in P\right)\to H=\left(p\in P⟼\bigcup F\left[p\right]\right)$$
4		imaeq2	$$⊢p=X\to F\left[p\right]=F\left[X\right]$$
5	4	unieqd	$$⊢p=X\to \bigcup F\left[p\right]=\bigcup F\left[X\right]$$
6	5	adantl	$$⊢\left(\left(\mathrm{Fun}F\wedge X\in P\right)\wedge p=X\right)\to \bigcup F\left[p\right]=\bigcup F\left[X\right]$$
7		simpr	$$⊢\left(\mathrm{Fun}F\wedge X\in P\right)\to X\in P$$
8		funimaexg	$$⊢\left(\mathrm{Fun}F\wedge X\in P\right)\to F\left[X\right]\in \mathrm{V}$$
9	8	uniexd	$$⊢\left(\mathrm{Fun}F\wedge X\in P\right)\to \bigcup F\left[X\right]\in \mathrm{V}$$
10	3 6 7 9	fvmptd	$$⊢\left(\mathrm{Fun}F\wedge X\in P\right)\to H\left(X\right)=\bigcup F\left[X\right]$$