Theorem quslem

Description: The function in qusval is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	qusval.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	qusval.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	qusval.f	$$⊢F=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
	qusval.e	$$⊢\phi \to \underset{\dot{}}{\sim }\in W$$
	qusval.r	$$⊢\phi \to R\in Z$$
Assertion	quslem	$$⊢\phi \to F:V\underset{onto}{⟶}V/\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		qusval.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
2		qusval.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		qusval.f	$$⊢F=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
4		qusval.e	$$⊢\phi \to \underset{\dot{}}{\sim }\in W$$
5		qusval.r	$$⊢\phi \to R\in Z$$
6		ecexg	$$⊢\underset{\dot{}}{\sim }\in W\to \left[x\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
7	4 6	syl	$$⊢\phi \to \left[x\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
8	7	ralrimivw	$$⊢\phi \to \forall x\in V\left[x\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
9	3	fnmpt	$$⊢\forall x\in V\left[x\right]\underset{\dot{}}{\sim }\in \mathrm{V}\to FFnV$$
10	8 9	syl	$$⊢\phi \to FFnV$$
11		dffn4	$$⊢FFnV\leftrightarrow F:V\underset{onto}{⟶}\mathrm{ran}F$$
12	10 11	sylib	$$⊢\phi \to F:V\underset{onto}{⟶}\mathrm{ran}F$$
13	3	rnmpt	$$⊢\mathrm{ran}F=\left\{y|\exists x\in Vy=\left[x\right]\underset{\dot{}}{\sim }\right\}$$
14		df-qs	$$⊢V/\underset{\dot{}}{\sim }=\left\{y|\exists x\in Vy=\left[x\right]\underset{\dot{}}{\sim }\right\}$$
15	13 14	eqtr4i	$$⊢\mathrm{ran}F=V/\underset{\dot{}}{\sim }$$
16		foeq3	$$⊢\mathrm{ran}F=V/\underset{\dot{}}{\sim }\to \left(F:V\underset{onto}{⟶}\mathrm{ran}F\leftrightarrow F:V\underset{onto}{⟶}V/\underset{\dot{}}{\sim }\right)$$
17	15 16	ax-mp	$$⊢F:V\underset{onto}{⟶}\mathrm{ran}F\leftrightarrow F:V\underset{onto}{⟶}V/\underset{\dot{}}{\sim }$$
18	12 17	sylib	$$⊢\phi \to F:V\underset{onto}{⟶}V/\underset{\dot{}}{\sim }$$