Theorem ecopover

Description: Assuming that operation F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation .~ , specified by the first hypothesis, is an equivalence relation. (Contributed by NM, 16-Feb-1996) (Revised by Mario Carneiro, 12-Aug-2015) (Proof shortened by AV, 1-May-2021)

	Ref	Expression
Hypotheses	ecopopr.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in \left(S\times S\right)\wedge y\in \left(S\times S\right)\right)\wedge \exists z\exists w\exists v\exists u\left(\left(x=⟨z,w⟩\wedge y=⟨v,u⟩\right)\wedge z\underset{\dot{}}{+}u=w\underset{\dot{}}{+}v\right)\right)\right\}$$
	ecopopr.com	$$⊢x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
	ecopopr.cl	$$⊢\left(x\in S\wedge y\in S\right)\to x\underset{\dot{}}{+}y\in S$$
	ecopopr.ass	$$⊢\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
	ecopopr.can	$$⊢\left(x\in S\wedge y\in S\right)\to \left(x\underset{\dot{}}{+}y=x\underset{\dot{}}{+}z\to y=z\right)$$
Assertion	ecopover	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}\left(S\times S\right)$$

Proof

Step	Hyp	Ref	Expression
1		ecopopr.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in \left(S\times S\right)\wedge y\in \left(S\times S\right)\right)\wedge \exists z\exists w\exists v\exists u\left(\left(x=⟨z,w⟩\wedge y=⟨v,u⟩\right)\wedge z\underset{\dot{}}{+}u=w\underset{\dot{}}{+}v\right)\right)\right\}$$
2		ecopopr.com	$$⊢x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
3		ecopopr.cl	$$⊢\left(x\in S\wedge y\in S\right)\to x\underset{\dot{}}{+}y\in S$$
4		ecopopr.ass	$$⊢\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
5		ecopopr.can	$$⊢\left(x\in S\wedge y\in S\right)\to \left(x\underset{\dot{}}{+}y=x\underset{\dot{}}{+}z\to y=z\right)$$
6	1	relopabiv	$$⊢\mathrm{Rel}\underset{\dot{}}{\sim }$$
7	1 2	ecopovsym	$$⊢f\underset{\dot{}}{\sim }g\to g\underset{\dot{}}{\sim }f$$
8	1 2 3 4 5	ecopovtrn	$$⊢\left(f\underset{\dot{}}{\sim }g\wedge g\underset{\dot{}}{\sim }h\right)\to f\underset{\dot{}}{\sim }h$$
9		vex	$$⊢g\in \mathrm{V}$$
10		vex	$$⊢h\in \mathrm{V}$$
11	9 10 2	caovcom	$$⊢g\underset{\dot{}}{+}h=h\underset{\dot{}}{+}g$$
12	1	ecopoveq	$$⊢\left(\left(g\in S\wedge h\in S\right)\wedge \left(g\in S\wedge h\in S\right)\right)\to \left(⟨g,h⟩\underset{\dot{}}{\sim }⟨g,h⟩\leftrightarrow g\underset{\dot{}}{+}h=h\underset{\dot{}}{+}g\right)$$
13	11 12	mpbiri	$$⊢\left(\left(g\in S\wedge h\in S\right)\wedge \left(g\in S\wedge h\in S\right)\right)\to ⟨g,h⟩\underset{\dot{}}{\sim }⟨g,h⟩$$
14	13	anidms	$$⊢\left(g\in S\wedge h\in S\right)\to ⟨g,h⟩\underset{\dot{}}{\sim }⟨g,h⟩$$
15	14	rgen2	$$⊢\forall g\in S\forall h\in S⟨g,h⟩\underset{\dot{}}{\sim }⟨g,h⟩$$
16		breq12	$$⊢\left(f=⟨g,h⟩\wedge f=⟨g,h⟩\right)\to \left(f\underset{\dot{}}{\sim }f\leftrightarrow ⟨g,h⟩\underset{\dot{}}{\sim }⟨g,h⟩\right)$$
17	16	anidms	$$⊢f=⟨g,h⟩\to \left(f\underset{\dot{}}{\sim }f\leftrightarrow ⟨g,h⟩\underset{\dot{}}{\sim }⟨g,h⟩\right)$$
18	17	ralxp	$$⊢\forall f\in \left(S\times S\right)f\underset{\dot{}}{\sim }f\leftrightarrow \forall g\in S\forall h\in S⟨g,h⟩\underset{\dot{}}{\sim }⟨g,h⟩$$
19	15 18	mpbir	$$⊢\forall f\in \left(S\times S\right)f\underset{\dot{}}{\sim }f$$
20	19	rspec	$$⊢f\in \left(S\times S\right)\to f\underset{\dot{}}{\sim }f$$
21		opabssxp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in \left(S\times S\right)\wedge y\in \left(S\times S\right)\right)\wedge \exists z\exists w\exists v\exists u\left(\left(x=⟨z,w⟩\wedge y=⟨v,u⟩\right)\wedge z\underset{\dot{}}{+}u=w\underset{\dot{}}{+}v\right)\right)\right\}\subseteq \left(S\times S\right)\times \left(S\times S\right)$$
22	1 21	eqsstri	$$⊢\underset{\dot{}}{\sim }\subseteq \left(S\times S\right)\times \left(S\times S\right)$$
23	22	ssbri	$$⊢f\underset{\dot{}}{\sim }f\to f\left(\left(S\times S\right)\times \left(S\times S\right)\right)f$$
24		brxp	$$⊢f\left(\left(S\times S\right)\times \left(S\times S\right)\right)f\leftrightarrow \left(f\in \left(S\times S\right)\wedge f\in \left(S\times S\right)\right)$$
25	24	simplbi	$$⊢f\left(\left(S\times S\right)\times \left(S\times S\right)\right)f\to f\in \left(S\times S\right)$$
26	23 25	syl	$$⊢f\underset{\dot{}}{\sim }f\to f\in \left(S\times S\right)$$
27	20 26	impbii	$$⊢f\in \left(S\times S\right)\leftrightarrow f\underset{\dot{}}{\sim }f$$
28	6 7 8 27	iseri	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}\left(S\times S\right)$$