Definition df-nq 8745

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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.) (New usage is discouraged.)

Assertion

Ref	Expression
df-nq	|- Q. = { x e. ( N. X. N. ) | A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-nq

Step	Hyp	Ref	Expression
1		cnq 8683	. 2 class Q.
2		vx	. . . . . . 7 set x
3	2	cv 1648	. . . . . 6 class x
4		vy	. . . . . . 7 set y
5	4	cv 1648	. . . . . 6 class y
6		ceq 8682	. . . . . 6 class ~Q
7	3, 5, 6	wbr 4172	. . . . 5 wff x ~Q y
8		c2nd 6307	. . . . . . . 8 class 2nd
9	5, 8	cfv 5413	. . . . . . 7 class ( 2nd ` y )
10	3, 8	cfv 5413	. . . . . . 7 class ( 2nd ` x )
11		clti 8678	. . . . . . 7 class <N
12	9, 10, 11	wbr 4172	. . . . . 6 wff ( 2nd ` y ) <N ( 2nd ` x )
13	12	wn 3	. . . . 5 wff -. ( 2nd ` y ) <N ( 2nd ` x )
14	7, 13	wi 4	. . . 4 wff ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) )
15		cnpi 8675	. . . . 5 class N.
16	15, 15	cxp 4835	. . . 4 class ( N. X. N. )
17	14, 4, 16	wral 2666	. . 3 wff A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) )
18	17, 2, 16	crab 2670	. 2 class { x e. ( N. X. N. ) | A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) }
19	1, 18	wceq 1649	1 wff Q. = { x e. ( N. X. N. ) | A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) }

This definition is referenced by:  nqex  8756  0nnq  8757  elpqn  8758  pinq  8760  nqereu  8762