Definition df-nqqs 6538

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 6470	. 2 class Q.
2		cnpi 6462	. . . 4 class N.
3	2, 2	cxp 4361	. . 3 class ( N. X. N. )
4		ceq 6469	. . 3 class ~Q
5	3, 4	cqs 6128	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1284	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  6553  0nnq  6554  1nq  6556  addpipqqs  6560  mulpipqqs  6563  ordpipqqs  6564  addclnq  6565  mulclnq  6566  dmaddpqlem  6567  nqpi  6568  addcomnqg  6571  addassnqg  6572  mulcomnqg  6573  mulassnqg  6574  distrnqg  6577  mulidnq  6579  recexnq  6580  nqtri3or  6586  ltsonq  6588  ltanqg  6590  ltmnqg  6591  ltexnqq  6598  prarloclemarch  6608  prarloclemarch2  6609  nnnq  6612  nqnq0  6631  nqpnq0nq  6643  prarloclemlt  6683  prarloclemlo  6684  prarloclemcalc  6692  nqprm  6732