Definition df-nqqs 7546

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 7478	. 2 class Q
2		cnpi 7470	. . . 4 class N
3	2, 2	cxp 4717	. . 3 class (N × N)
4		ceq 7477	. . 3 class ~Q
5	3, 4	cqs 6687	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1395	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7561  0nnq  7562  1nq  7564  addpipqqs  7568  mulpipqqs  7571  ordpipqqs  7572  addclnq  7573  mulclnq  7574  dmaddpqlem  7575  nqpi  7576  addcomnqg  7579  addassnqg  7580  mulcomnqg  7581  mulassnqg  7582  distrnqg  7585  mulidnq  7587  recexnq  7588  nqtri3or  7594  ltsonq  7596  ltanqg  7598  ltmnqg  7599  ltexnqq  7606  prarloclemarch  7616  prarloclemarch2  7617  nnnq  7620  nqnq0  7639  nqpnq0nq  7651  prarloclemlt  7691  prarloclemlo  7692  prarloclemcalc  7700  nqprm  7740