Theorem eroprf2

Description: Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	eropr2.1	$$⊢J=A/\underset{\dot{}}{\sim }$$
	eropr2.2	$$⊢\underset{\dot{}}{⨣}=\left\{⟨⟨x,y⟩,z⟩|\exists p\in A\exists q\in A\left(\left(x=\left[p\right]\underset{\dot{}}{\sim }\wedge y=\left[q\right]\underset{\dot{}}{\sim }\right)\wedge z=\left[\left(p\underset{\dot{}}{+}q\right)\right]\underset{\dot{}}{\sim }\right)\right\}$$
	eropr2.3	$$⊢\phi \to \underset{\dot{}}{\sim }\in X$$
	eropr2.4	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}U$$
	eropr2.5	$$⊢\phi \to A\subseteq U$$
	eropr2.6	$$⊢\phi \to \underset{\dot{}}{+}:A\times A⟶A$$
	eropr2.7	$$⊢\left(\phi \wedge \left(\left(r\in A\wedge s\in A\right)\wedge \left(t\in A\wedge u\in A\right)\right)\right)\to \left(\left(r\underset{\dot{}}{\sim }s\wedge t\underset{\dot{}}{\sim }u\right)\to \left(r\underset{\dot{}}{+}t\right)\underset{\dot{}}{\sim }\left(s\underset{\dot{}}{+}u\right)\right)$$
Assertion	eroprf2	$$⊢\phi \to \underset{\dot{}}{⨣}:J\times J⟶J$$

Proof

Step	Hyp	Ref	Expression
1		eropr2.1	$$⊢J=A/\underset{\dot{}}{\sim }$$
2		eropr2.2	$$⊢\underset{\dot{}}{⨣}=\left\{⟨⟨x,y⟩,z⟩|\exists p\in A\exists q\in A\left(\left(x=\left[p\right]\underset{\dot{}}{\sim }\wedge y=\left[q\right]\underset{\dot{}}{\sim }\right)\wedge z=\left[\left(p\underset{\dot{}}{+}q\right)\right]\underset{\dot{}}{\sim }\right)\right\}$$
3		eropr2.3	$$⊢\phi \to \underset{\dot{}}{\sim }\in X$$
4		eropr2.4	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}U$$
5		eropr2.5	$$⊢\phi \to A\subseteq U$$
6		eropr2.6	$$⊢\phi \to \underset{\dot{}}{+}:A\times A⟶A$$
7		eropr2.7	$$⊢\left(\phi \wedge \left(\left(r\in A\wedge s\in A\right)\wedge \left(t\in A\wedge u\in A\right)\right)\right)\to \left(\left(r\underset{\dot{}}{\sim }s\wedge t\underset{\dot{}}{\sim }u\right)\to \left(r\underset{\dot{}}{+}t\right)\underset{\dot{}}{\sim }\left(s\underset{\dot{}}{+}u\right)\right)$$
8	1 1 3 4 4 4 5 5 5 6 7 2 3 3 1	eroprf	$$⊢\phi \to \underset{\dot{}}{⨣}:J\times J⟶J$$