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	|- ~R Er ( P. X. P. )

Proof

Step	Hyp	Ref	Expression
1		df-enr	|- ~R = { <. x , y >. | ( ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) ) ) }
2		addcompr	|- ( x +P. y ) = ( y +P. x )
3		addclpr	|- ( ( x e. P. /\ y e. P. ) -> ( x +P. y ) e. P. )
4		addasspr	|- ( ( x +P. y ) +P. z ) = ( x +P. ( y +P. z ) )
5		addcanpr	|- ( ( x e. P. /\ y e. P. ) -> ( ( x +P. y ) = ( x +P. z ) -> y = z ) )
6	1 2 3 4 5	ecopover	|- ~R Er ( P. X. P. )