Definition df-nqqs 6418

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. X. N. ) /. ~Q )

Detailed syntax breakdown of Definition df-nqqs

Step	Hyp	Ref	Expression
1		cnq 6350	. 2 class Q.
2		cnpi 6342	. . . 4 class N.
3	2, 2	cxp 4321	. . 3 class ( N. X. N. )
4		ceq 6349	. . 3 class ~Q
5	3, 4	cqs 6083	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1243	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  6433  0nnq  6434  1nq  6436  addpipqqs  6440  mulpipqqs  6443  ordpipqqs  6444  addclnq  6445  mulclnq  6446  dmaddpqlem  6447  nqpi  6448  addcomnqg  6451  addassnqg  6452  mulcomnqg  6453  mulassnqg  6454  distrnqg  6457  mulidnq  6459  recexnq  6460  nqtri3or  6466  ltsonq  6468  ltanqg  6470  ltmnqg  6471  ltexnqq  6478  prarloclemarch  6488  prarloclemarch2  6489  nnnq  6492  nqnq0  6511  nqpnq0nq  6523  prarloclemlt  6563  prarloclemlo  6564  prarloclemcalc  6572  nqprm  6612