Definition df-nqqs 7156

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 7088	. 2 class Q.
2		cnpi 7080	. . . 4 class N.
3	2, 2	cxp 4537	. . 3 class ( N. X. N. )
4		ceq 7087	. . 3 class ~Q
5	3, 4	cqs 6428	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1331	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7171  0nnq  7172  1nq  7174  addpipqqs  7178  mulpipqqs  7181  ordpipqqs  7182  addclnq  7183  mulclnq  7184  dmaddpqlem  7185  nqpi  7186  addcomnqg  7189  addassnqg  7190  mulcomnqg  7191  mulassnqg  7192  distrnqg  7195  mulidnq  7197  recexnq  7198  nqtri3or  7204  ltsonq  7206  ltanqg  7208  ltmnqg  7209  ltexnqq  7216  prarloclemarch  7226  prarloclemarch2  7227  nnnq  7230  nqnq0  7249  nqpnq0nq  7261  prarloclemlt  7301  prarloclemlo  7302  prarloclemcalc  7310  nqprm  7350