Definition df-nqqs 7535

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 7467	. 2 class Q.
2		cnpi 7459	. . . 4 class N.
3	2, 2	cxp 4717	. . 3 class ( N. X. N. )
4		ceq 7466	. . 3 class ~Q
5	3, 4	cqs 6679	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1395	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7550  0nnq  7551  1nq  7553  addpipqqs  7557  mulpipqqs  7560  ordpipqqs  7561  addclnq  7562  mulclnq  7563  dmaddpqlem  7564  nqpi  7565  addcomnqg  7568  addassnqg  7569  mulcomnqg  7570  mulassnqg  7571  distrnqg  7574  mulidnq  7576  recexnq  7577  nqtri3or  7583  ltsonq  7585  ltanqg  7587  ltmnqg  7588  ltexnqq  7595  prarloclemarch  7605  prarloclemarch2  7606  nnnq  7609  nqnq0  7628  nqpnq0nq  7640  prarloclemlt  7680  prarloclemlo  7681  prarloclemcalc  7689  nqprm  7729