Definition df-nqqs 7461

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 7393	. 2 class Q
2		cnpi 7385	. . . 4 class N
3	2, 2	cxp 4673	. . 3 class (N × N)
4		ceq 7392	. . 3 class ~Q
5	3, 4	cqs 6619	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1373	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7476  0nnq  7477  1nq  7479  addpipqqs  7483  mulpipqqs  7486  ordpipqqs  7487  addclnq  7488  mulclnq  7489  dmaddpqlem  7490  nqpi  7491  addcomnqg  7494  addassnqg  7495  mulcomnqg  7496  mulassnqg  7497  distrnqg  7500  mulidnq  7502  recexnq  7503  nqtri3or  7509  ltsonq  7511  ltanqg  7513  ltmnqg  7514  ltexnqq  7521  prarloclemarch  7531  prarloclemarch2  7532  nnnq  7535  nqnq0  7554  nqpnq0nq  7566  prarloclemlt  7606  prarloclemlo  7607  prarloclemcalc  7615  nqprm  7655