Theorem fundcmpsurinjlem1

Description: Lemma 1 for fundcmpsurinj . (Contributed by AV, 4-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.g	$$⊢G=\left(x\in A⟼F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right)$$
Assertion	fundcmpsurinjlem1	$$⊢\mathrm{ran}G=P$$

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.g	$$⊢G=\left(x\in A⟼F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right)$$
3	2	rnmpt	$$⊢\mathrm{ran}G=\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}$$
4	3 1	eqtr4i	$$⊢\mathrm{ran}G=P$$