Definition df-nqqs 7408

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 7340	. 2 class Q
2		cnpi 7332	. . . 4 class N
3	2, 2	cxp 4657	. . 3 class (N × N)
4		ceq 7339	. . 3 class ~Q
5	3, 4	cqs 6586	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1364	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7423  0nnq  7424  1nq  7426  addpipqqs  7430  mulpipqqs  7433  ordpipqqs  7434  addclnq  7435  mulclnq  7436  dmaddpqlem  7437  nqpi  7438  addcomnqg  7441  addassnqg  7442  mulcomnqg  7443  mulassnqg  7444  distrnqg  7447  mulidnq  7449  recexnq  7450  nqtri3or  7456  ltsonq  7458  ltanqg  7460  ltmnqg  7461  ltexnqq  7468  prarloclemarch  7478  prarloclemarch2  7479  nnnq  7482  nqnq0  7501  nqpnq0nq  7513  prarloclemlt  7553  prarloclemlo  7554  prarloclemcalc  7562  nqprm  7602