Definition df-nqqs 7567

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 7499	. 2 class Q
2		cnpi 7491	. . . 4 class N
3	2, 2	cxp 4723	. . 3 class (N × N)
4		ceq 7498	. . 3 class ~Q
5	3, 4	cqs 6700	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1397	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7582  0nnq  7583  1nq  7585  addpipqqs  7589  mulpipqqs  7592  ordpipqqs  7593  addclnq  7594  mulclnq  7595  dmaddpqlem  7596  nqpi  7597  addcomnqg  7600  addassnqg  7601  mulcomnqg  7602  mulassnqg  7603  distrnqg  7606  mulidnq  7608  recexnq  7609  nqtri3or  7615  ltsonq  7617  ltanqg  7619  ltmnqg  7620  ltexnqq  7627  prarloclemarch  7637  prarloclemarch2  7638  nnnq  7641  nqnq0  7660  nqpnq0nq  7672  prarloclemlt  7712  prarloclemlo  7713  prarloclemcalc  7721  nqprm  7761