Definition df-nqqs 7262

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 7194	. 2 class Q.
2		cnpi 7186	. . . 4 class N.
3	2, 2	cxp 4583	. . 3 class ( N. X. N. )
4		ceq 7193	. . 3 class ~Q
5	3, 4	cqs 6476	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1335	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7277  0nnq  7278  1nq  7280  addpipqqs  7284  mulpipqqs  7287  ordpipqqs  7288  addclnq  7289  mulclnq  7290  dmaddpqlem  7291  nqpi  7292  addcomnqg  7295  addassnqg  7296  mulcomnqg  7297  mulassnqg  7298  distrnqg  7301  mulidnq  7303  recexnq  7304  nqtri3or  7310  ltsonq  7312  ltanqg  7314  ltmnqg  7315  ltexnqq  7322  prarloclemarch  7332  prarloclemarch2  7333  nnnq  7336  nqnq0  7355  nqpnq0nq  7367  prarloclemlt  7407  prarloclemlo  7408  prarloclemcalc  7416  nqprm  7456