Theorem 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	$$⊢{~}_{𝑹}\mathrm{Er}\left(𝑷\times 𝑷\right)$$

Proof

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