ecopovsym

Description: Assuming the operation F is commutative, show that the relation .~ , specified by the first hypothesis, is symmetric. (Contributed by NM, 27-Aug-1995) (Revised by Mario Carneiro, 26-Apr-2015)

	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$
Assertion	ecopovsym	$⊢ A \underset{˙}{\sim} B \to B \underset{˙}{\sim} A$

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		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)$
4	1 3	eqsstri	$⊢ \underset{˙}{\sim} \subseteq (S \times S) \times (S \times S)$
5	4	brel	$⊢ A \underset{˙}{\sim} B \to (A \in (S \times S) \land B \in (S \times S))$
6		eqid	$⊢ S \times S = S \times S$
7		breq1	$⊢ ⟨f, g⟩ = A \to (⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow A \underset{˙}{\sim} ⟨h, t⟩)$
8		breq2	$⊢ ⟨f, g⟩ = A \to (⟨h, t⟩ \underset{˙}{\sim} ⟨f, g⟩ \leftrightarrow ⟨h, t⟩ \underset{˙}{\sim} A)$
9	7 8	bibi12d	$⊢ ⟨f, g⟩ = A \to ((⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow ⟨h, t⟩ \underset{˙}{\sim} ⟨f, g⟩) \leftrightarrow (A \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow ⟨h, t⟩ \underset{˙}{\sim} A))$
10		breq2	$⊢ ⟨h, t⟩ = B \to (A \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow A \underset{˙}{\sim} B)$
11		breq1	$⊢ ⟨h, t⟩ = B \to (⟨h, t⟩ \underset{˙}{\sim} A \leftrightarrow B \underset{˙}{\sim} A)$
12	10 11	bibi12d	$⊢ ⟨h, t⟩ = B \to ((A \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow ⟨h, t⟩ \underset{˙}{\sim} A) \leftrightarrow (A \underset{˙}{\sim} B \leftrightarrow B \underset{˙}{\sim} A))$
13	1	ecopoveq	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S)) \to (⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow f \underset{˙}{+} t = g \underset{˙}{+} h)$
14		vex	$⊢ f \in V$
15		vex	$⊢ t \in V$
16	14 15 2	caovcom	$⊢ f \underset{˙}{+} t = t \underset{˙}{+} f$
17		vex	$⊢ g \in V$
18		vex	$⊢ h \in V$
19	17 18 2	caovcom	$⊢ g \underset{˙}{+} h = h \underset{˙}{+} g$
20	16 19	eqeq12i	$⊢ f \underset{˙}{+} t = g \underset{˙}{+} h \leftrightarrow t \underset{˙}{+} f = h \underset{˙}{+} g$
21		eqcom	$⊢ t \underset{˙}{+} f = h \underset{˙}{+} g \leftrightarrow h \underset{˙}{+} g = t \underset{˙}{+} f$
22	20 21	bitri	$⊢ f \underset{˙}{+} t = g \underset{˙}{+} h \leftrightarrow h \underset{˙}{+} g = t \underset{˙}{+} f$
23	13 22	syl6bb	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S)) \to (⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow h \underset{˙}{+} g = t \underset{˙}{+} f)$
24	1	ecopoveq	$⊢ ((h \in S \land t \in S) \land (f \in S \land g \in S)) \to (⟨h, t⟩ \underset{˙}{\sim} ⟨f, g⟩ \leftrightarrow h \underset{˙}{+} g = t \underset{˙}{+} f)$
25	24	ancoms	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S)) \to (⟨h, t⟩ \underset{˙}{\sim} ⟨f, g⟩ \leftrightarrow h \underset{˙}{+} g = t \underset{˙}{+} f)$
26	23 25	bitr4d	$⊢ ((f \in S \land g \in S) \land (h \in S \land t \in S)) \to (⟨f, g⟩ \underset{˙}{\sim} ⟨h, t⟩ \leftrightarrow ⟨h, t⟩ \underset{˙}{\sim} ⟨f, g⟩)$
27	6 9 12 26	2optocl	$⊢ (A \in (S \times S) \land B \in (S \times S)) \to (A \underset{˙}{\sim} B \leftrightarrow B \underset{˙}{\sim} A)$
28	5 27	syl	$⊢ A \underset{˙}{\sim} B \to (A \underset{˙}{\sim} B \leftrightarrow B \underset{˙}{\sim} A)$
29	28	ibi	$⊢ A \underset{˙}{\sim} B \to B \underset{˙}{\sim} A$

Metamath Proof Explorer

Theorem ecopovsym

Proof