Definition df-nqqs 7434

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 7366	. 2 class Q
2		cnpi 7358	. . . 4 class N
3	2, 2	cxp 4662	. . 3 class (N × N)
4		ceq 7365	. . 3 class ~Q
5	3, 4	cqs 6600	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1364	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7449  0nnq  7450  1nq  7452  addpipqqs  7456  mulpipqqs  7459  ordpipqqs  7460  addclnq  7461  mulclnq  7462  dmaddpqlem  7463  nqpi  7464  addcomnqg  7467  addassnqg  7468  mulcomnqg  7469  mulassnqg  7470  distrnqg  7473  mulidnq  7475  recexnq  7476  nqtri3or  7482  ltsonq  7484  ltanqg  7486  ltmnqg  7487  ltexnqq  7494  prarloclemarch  7504  prarloclemarch2  7505  nnnq  7508  nqnq0  7527  nqpnq0nq  7539  prarloclemlt  7579  prarloclemlo  7580  prarloclemcalc  7588  nqprm  7628