Definition df-nqqs 7463

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 7395	. 2 class Q.
2		cnpi 7387	. . . 4 class N.
3	2, 2	cxp 4674	. . 3 class ( N. X. N. )
4		ceq 7394	. . 3 class ~Q
5	3, 4	cqs 6621	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1373	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7478  0nnq  7479  1nq  7481  addpipqqs  7485  mulpipqqs  7488  ordpipqqs  7489  addclnq  7490  mulclnq  7491  dmaddpqlem  7492  nqpi  7493  addcomnqg  7496  addassnqg  7497  mulcomnqg  7498  mulassnqg  7499  distrnqg  7502  mulidnq  7504  recexnq  7505  nqtri3or  7511  ltsonq  7513  ltanqg  7515  ltmnqg  7516  ltexnqq  7523  prarloclemarch  7533  prarloclemarch2  7534  nnnq  7537  nqnq0  7556  nqpnq0nq  7568  prarloclemlt  7608  prarloclemlo  7609  prarloclemcalc  7617  nqprm  7657