Definition df-nqqs 7568

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

This definition is referenced by:  nqex  7583  0nnq  7584  1nq  7586  addpipqqs  7590  mulpipqqs  7593  ordpipqqs  7594  addclnq  7595  mulclnq  7596  dmaddpqlem  7597  nqpi  7598  addcomnqg  7601  addassnqg  7602  mulcomnqg  7603  mulassnqg  7604  distrnqg  7607  mulidnq  7609  recexnq  7610  nqtri3or  7616  ltsonq  7618  ltanqg  7620  ltmnqg  7621  ltexnqq  7628  prarloclemarch  7638  prarloclemarch2  7639  nnnq  7642  nqnq0  7661  nqpnq0nq  7673  prarloclemlt  7713  prarloclemlo  7714  prarloclemcalc  7722  nqprm  7762