Definition df-nqqs 7681

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.2 of [Gleason] p. 117. (Contributed by NM, 16-Aug-1995.)

Assertion

Ref	Expression
df-nqqs	⊢ Q = ((N × N) / ~Q )

Detailed syntax breakdown of Definition df-nqqs

Step	Hyp	Ref	Expression
1		cnq 7613	. 2 class Q
2		cnpi 7605	. . . 4 class N
3	2, 2	cxp 4754	. . 3 class (N × N)
4		ceq 7612	. . 3 class ~Q
5	3, 4	cqs 6781	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1398	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7696  0nnq  7697  1nq  7699  addpipqqs  7703  mulpipqqs  7706  ordpipqqs  7707  addclnq  7708  mulclnq  7709  dmaddpqlem  7710  nqpi  7711  addcomnqg  7714  addassnqg  7715  mulcomnqg  7716  mulassnqg  7717  distrnqg  7720  mulidnq  7722  recexnq  7723  nqtri3or  7729  ltsonq  7731  ltanqg  7733  ltmnqg  7734  ltexnqq  7741  prarloclemarch  7751  prarloclemarch2  7752  nnnq  7755  nqnq0  7774  nqpnq0nq  7786  prarloclemlt  7826  prarloclemlo  7827  prarloclemcalc  7835  nqprm  7875