Definition df-nqqs 7663

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 7595	. 2 class Q
2		cnpi 7587	. . . 4 class N
3	2, 2	cxp 4747	. . 3 class (N × N)
4		ceq 7594	. . 3 class ~Q
5	3, 4	cqs 6766	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1398	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7678  0nnq  7679  1nq  7681  addpipqqs  7685  mulpipqqs  7688  ordpipqqs  7689  addclnq  7690  mulclnq  7691  dmaddpqlem  7692  nqpi  7693  addcomnqg  7696  addassnqg  7697  mulcomnqg  7698  mulassnqg  7699  distrnqg  7702  mulidnq  7704  recexnq  7705  nqtri3or  7711  ltsonq  7713  ltanqg  7715  ltmnqg  7716  ltexnqq  7723  prarloclemarch  7733  prarloclemarch2  7734  nnnq  7737  nqnq0  7756  nqpnq0nq  7768  prarloclemlt  7808  prarloclemlo  7809  prarloclemcalc  7817  nqprm  7857