Definition df-nqqs 7496

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 7428	. 2 class Q
2		cnpi 7420	. . . 4 class N
3	2, 2	cxp 4691	. . 3 class (N × N)
4		ceq 7427	. . 3 class ~Q
5	3, 4	cqs 6642	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1373	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7511  0nnq  7512  1nq  7514  addpipqqs  7518  mulpipqqs  7521  ordpipqqs  7522  addclnq  7523  mulclnq  7524  dmaddpqlem  7525  nqpi  7526  addcomnqg  7529  addassnqg  7530  mulcomnqg  7531  mulassnqg  7532  distrnqg  7535  mulidnq  7537  recexnq  7538  nqtri3or  7544  ltsonq  7546  ltanqg  7548  ltmnqg  7549  ltexnqq  7556  prarloclemarch  7566  prarloclemarch2  7567  nnnq  7570  nqnq0  7589  nqpnq0nq  7601  prarloclemlt  7641  prarloclemlo  7642  prarloclemcalc  7650  nqprm  7690