Definition df-nqqs 6503

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 6435	. 2 class Q.
2		cnpi 6427	. . . 4 class N.
3	2, 2	cxp 4370	. . 3 class ( N. X. N. )
4		ceq 6434	. . 3 class ~Q
5	3, 4	cqs 6135	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1259	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  6518  0nnq  6519  1nq  6521  addpipqqs  6525  mulpipqqs  6528  ordpipqqs  6529  addclnq  6530  mulclnq  6531  dmaddpqlem  6532  nqpi  6533  addcomnqg  6536  addassnqg  6537  mulcomnqg  6538  mulassnqg  6539  distrnqg  6542  mulidnq  6544  recexnq  6545  nqtri3or  6551  ltsonq  6553  ltanqg  6555  ltmnqg  6556  ltexnqq  6563  prarloclemarch  6573  prarloclemarch2  6574  nnnq  6577  nqnq0  6596  nqpnq0nq  6608  prarloclemlt  6648  prarloclemlo  6649  prarloclemcalc  6657  nqprm  6697