Definition df-nqqs 7721

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 7653	. 2 class Q.
2		cnpi 7645	. . . 4 class N.
3	2, 2	cxp 4774	. . 3 class ( N. X. N. )
4		ceq 7652	. . 3 class ~Q
5	3, 4	cqs 6810	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1402	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is used by:  nqex  7736  0nnq  7737  1nq  7739  addpipqqs  7743  mulpipqqs  7746  ordpipqqs  7747  addclnq  7748  mulclnq  7749  dmaddpqlem  7750  nqpi  7751  addcomnqg  7754  addassnqg  7755  mulcomnqg  7756  mulassnqg  7757  distrnqg  7760  mulidnq  7762  recexnq  7763  nqtri3or  7769  ltsonq  7771  ltanqg  7773  ltmnqg  7774  ltexnqq  7781  prarloclemarch  7791  prarloclemarch2  7792  nnnq  7795  nqnq0  7814  nqpnq0nq  7826  prarloclemlt  7866  prarloclemlo  7867  prarloclemcalc  7875  nqprm  7915