Definition df-nr 3961

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 4034, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126.

Assertion

Ref	Expression
df-nr	|- R. = ((P. X. P.)/. ~R )

Detailed syntax breakdown of Definition df-nr

Step	Hyp	Ref	Expression
1		cnr 3787	. 2 class R.
2		cnp 3779	. . . 4 class P.
3	2, 2	cxp 2408	. . 3 class (P. X. P.)
4		cer 3786	. . 3 class ~R
5	3, 4	cqs 3199	. 2 class ((P. X. P.)/. ~R )
6	1, 5	wceq 1091	1 wff R. = ((P. X. P.)/. ~R )

This definition is referenced by:  srex 3973  addsrpr 3978  mulsrpr 3979  ltsrpr 3980  0nsr 3982  0r 3983  1r 3984  m1r 3985  addclsr 3986  mulclsr 3987  addcomsr 3990  addasssr 3991  mulcomsr 3992  mulasssr 3993  distrsr 3994  ltsosr 3997  0idsr 4000  1idsr 4001  00sr 4002  ltasr 4003  recexsrlem 4006  mulgt0sr 4008  map2psrpr 4014

metamath.org