Definition df-nqqs 7377

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 7309	. 2 class Q
2		cnpi 7301	. . . 4 class N
3	2, 2	cxp 4642	. . 3 class (N × N)
4		ceq 7308	. . 3 class ~Q
5	3, 4	cqs 6558	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1364	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7392  0nnq  7393  1nq  7395  addpipqqs  7399  mulpipqqs  7402  ordpipqqs  7403  addclnq  7404  mulclnq  7405  dmaddpqlem  7406  nqpi  7407  addcomnqg  7410  addassnqg  7411  mulcomnqg  7412  mulassnqg  7413  distrnqg  7416  mulidnq  7418  recexnq  7419  nqtri3or  7425  ltsonq  7427  ltanqg  7429  ltmnqg  7430  ltexnqq  7437  prarloclemarch  7447  prarloclemarch2  7448  nnnq  7451  nqnq0  7470  nqpnq0nq  7482  prarloclemlt  7522  prarloclemlo  7523  prarloclemcalc  7531  nqprm  7571