Definition df-nqqs 7325

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 7257	. 2 class Q
2		cnpi 7249	. . . 4 class N
3	2, 2	cxp 4620	. . 3 class (N × N)
4		ceq 7256	. . 3 class ~Q
5	3, 4	cqs 6527	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1353	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7340  0nnq  7341  1nq  7343  addpipqqs  7347  mulpipqqs  7350  ordpipqqs  7351  addclnq  7352  mulclnq  7353  dmaddpqlem  7354  nqpi  7355  addcomnqg  7358  addassnqg  7359  mulcomnqg  7360  mulassnqg  7361  distrnqg  7364  mulidnq  7366  recexnq  7367  nqtri3or  7373  ltsonq  7375  ltanqg  7377  ltmnqg  7378  ltexnqq  7385  prarloclemarch  7395  prarloclemarch2  7396  nnnq  7399  nqnq0  7418  nqpnq0nq  7430  prarloclemlt  7470  prarloclemlo  7471  prarloclemcalc  7479  nqprm  7519