Theorem qusaddflem

Description: The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	qusaddf.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	qusaddf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	qusaddf.r	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}V$$
	qusaddf.z	$$⊢\phi \to R\in Z$$
	qusaddf.e	$$⊢\phi \to \left(\left(a\underset{\dot{}}{\sim }p\wedge b\underset{\dot{}}{\sim }q\right)\to \left(a\underset{\dot{}}{·}b\right)\underset{\dot{}}{\sim }\left(p\underset{\dot{}}{·}q\right)\right)$$
	qusaddf.c	$$⊢\left(\phi \wedge \left(p\in V\wedge q\in V\right)\right)\to p\underset{\dot{}}{·}q\in V$$
	qusaddflem.f	$$⊢F=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
	qusaddflem.g	$$⊢\phi \to \underset{\dot{}}{\bullet }=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
Assertion	qusaddflem	$$⊢\phi \to \underset{\dot{}}{\bullet }:\left(V/\underset{\dot{}}{\sim }\right)\times \left(V/\underset{\dot{}}{\sim }\right)⟶V/\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		qusaddf.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
2		qusaddf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		qusaddf.r	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}V$$
4		qusaddf.z	$$⊢\phi \to R\in Z$$
5		qusaddf.e	$$⊢\phi \to \left(\left(a\underset{\dot{}}{\sim }p\wedge b\underset{\dot{}}{\sim }q\right)\to \left(a\underset{\dot{}}{·}b\right)\underset{\dot{}}{\sim }\left(p\underset{\dot{}}{·}q\right)\right)$$
6		qusaddf.c	$$⊢\left(\phi \wedge \left(p\in V\wedge q\in V\right)\right)\to p\underset{\dot{}}{·}q\in V$$
7		qusaddflem.f	$$⊢F=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
8		qusaddflem.g	$$⊢\phi \to \underset{\dot{}}{\bullet }=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
9		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
10	2 9	syl6eqel	$$⊢\phi \to V\in \mathrm{V}$$
11		erex	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}V\to \left(V\in \mathrm{V}\to \underset{\dot{}}{\sim }\in \mathrm{V}\right)$$
12	3 10 11	sylc	$$⊢\phi \to \underset{\dot{}}{\sim }\in \mathrm{V}$$
13	1 2 7 12 4	quslem	$$⊢\phi \to F:V\underset{onto}{⟶}V/\underset{\dot{}}{\sim }$$
14	3 10 7 6 5	ercpbl	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\wedge \left(p\in V\wedge q\in V\right)\right)\to \left(\left(F\left(a\right)=F\left(p\right)\wedge F\left(b\right)=F\left(q\right)\right)\to F\left(a\underset{\dot{}}{·}b\right)=F\left(p\underset{\dot{}}{·}q\right)\right)$$
15	13 14 8 6	imasaddflem	$$⊢\phi \to \underset{\dot{}}{\bullet }:\left(V/\underset{\dot{}}{\sim }\right)\times \left(V/\underset{\dot{}}{\sim }\right)⟶V/\underset{\dot{}}{\sim }$$