Definition df-nqqs 7180

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 × N) / ~Q )

Detailed syntax breakdown of Definition df-nqqs

Step	Hyp	Ref	Expression
1		cnq 7112	. 2 class Q
2		cnpi 7104	. . . 4 class N
3	2, 2	cxp 4545	. . 3 class (N × N)
4		ceq 7111	. . 3 class ~Q
5	3, 4	cqs 6436	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1332	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7195  0nnq  7196  1nq  7198  addpipqqs  7202  mulpipqqs  7205  ordpipqqs  7206  addclnq  7207  mulclnq  7208  dmaddpqlem  7209  nqpi  7210  addcomnqg  7213  addassnqg  7214  mulcomnqg  7215  mulassnqg  7216  distrnqg  7219  mulidnq  7221  recexnq  7222  nqtri3or  7228  ltsonq  7230  ltanqg  7232  ltmnqg  7233  ltexnqq  7240  prarloclemarch  7250  prarloclemarch2  7251  nnnq  7254  nqnq0  7273  nqpnq0nq  7285  prarloclemlt  7325  prarloclemlo  7326  prarloclemcalc  7334  nqprm  7374