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{˙}{\sim} = \{⟨x, y⟩ \| ((x \in (S \times S) \land y \in (S \times S)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \underset{˙}{+} u = w \underset{˙}{+} v))\}$
	ecopopr.com	$⊢ x \underset{˙}{+} y = y \underset{˙}{+} x$
	ecopopr.cl	$⊢ (x \in S \land y \in S) \to x \underset{˙}{+} y \in S$
	ecopopr.ass	$⊢ (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
	ecopopr.can	$⊢ (x \in S \land y \in S) \to (x \underset{˙}{+} y = x \underset{˙}{+} z \to y = z)$
Assertion	ecopover	$⊢ \underset{˙}{\sim} Er (S \times S)$

Proof

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

Metamath Proof Explorer

Theorem ecopover

Proof