Definition df-nqqs 7349

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 7281	. 2 class Q.
2		cnpi 7273	. . . 4 class N.
3	2, 2	cxp 4626	. . 3 class ( N. X. N. )
4		ceq 7280	. . 3 class ~Q
5	3, 4	cqs 6536	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1353	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7364  0nnq  7365  1nq  7367  addpipqqs  7371  mulpipqqs  7374  ordpipqqs  7375  addclnq  7376  mulclnq  7377  dmaddpqlem  7378  nqpi  7379  addcomnqg  7382  addassnqg  7383  mulcomnqg  7384  mulassnqg  7385  distrnqg  7388  mulidnq  7390  recexnq  7391  nqtri3or  7397  ltsonq  7399  ltanqg  7401  ltmnqg  7402  ltexnqq  7409  prarloclemarch  7419  prarloclemarch2  7420  nnnq  7423  nqnq0  7442  nqpnq0nq  7454  prarloclemlt  7494  prarloclemlo  7495  prarloclemcalc  7503  nqprm  7543