Definition df-nqqs 7665

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 7597	. 2 class Q.
2		cnpi 7589	. . . 4 class N.
3	2, 2	cxp 4749	. . 3 class ( N. X. N. )
4		ceq 7596	. . 3 class ~Q
5	3, 4	cqs 6768	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1398	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7680  0nnq  7681  1nq  7683  addpipqqs  7687  mulpipqqs  7690  ordpipqqs  7691  addclnq  7692  mulclnq  7693  dmaddpqlem  7694  nqpi  7695  addcomnqg  7698  addassnqg  7699  mulcomnqg  7700  mulassnqg  7701  distrnqg  7704  mulidnq  7706  recexnq  7707  nqtri3or  7713  ltsonq  7715  ltanqg  7717  ltmnqg  7718  ltexnqq  7725  prarloclemarch  7735  prarloclemarch2  7736  nnnq  7739  nqnq0  7758  nqpnq0nq  7770  prarloclemlt  7810  prarloclemlo  7811  prarloclemcalc  7819  nqprm  7859