enrer

Description: The equivalence relation for signed reals is an equivalence relation. Proposition 9-4.1 of Gleason p. 126. (Contributed by NM, 3-Sep-1995) (Revised by Mario Carneiro, 6-Jul-2015) (New usage is discouraged.)

		Ref	Expression
	Assertion	enrer	$⊢ ~_{𝑹} Er (𝑷 \times 𝑷)$

Proof

Step	Hyp	Ref	Expression
1		df-enr	$⊢ ~_{𝑹} = \{⟨x, y⟩ \| ((x \in (𝑷 \times 𝑷) \land y \in (𝑷 \times 𝑷)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z +_{𝑷} u = w +_{𝑷} v))\}$
2		addcompr	$⊢ x +_{𝑷} y = y +_{𝑷} x$
3		addclpr	$⊢ (x \in 𝑷 \land y \in 𝑷) \to x +_{𝑷} y \in 𝑷$
4		addasspr	$⊢ (x +_{𝑷} y) +_{𝑷} z = x +_{𝑷} (y +_{𝑷} z)$
5		addcanpr	$⊢ (x \in 𝑷 \land y \in 𝑷) \to (x +_{𝑷} y = x +_{𝑷} z \to y = z)$
6	1 2 3 4 5	ecopover	$⊢ ~_{𝑹} Er (𝑷 \times 𝑷)$

Metamath Proof Explorer

Theorem enrer

Proof