Definition df-nq 9289

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 9497, 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 9229	. 2 class Q.
2		vx	. . . . . . 7 setvar x
3	2	cv 1378	. . . . . 6 class x
4		vy	. . . . . . 7 setvar y
5	4	cv 1378	. . . . . 6 class y
6		ceq 9228	. . . . . 6 class ~Q
7	3, 5, 6	wbr 4447	. . . . 5 wff x ~Q y
8		c2nd 6783	. . . . . . . 8 class 2nd
9	5, 8	cfv 5587	. . . . . . 7 class ( 2nd ` y )
10	3, 8	cfv 5587	. . . . . . 7 class ( 2nd ` x )
11		clti 9224	. . . . . . 7 class <N
12	9, 10, 11	wbr 4447	. . . . . 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 9221	. . . . 5 class N.
16	15, 15	cxp 4997	. . . 4 class ( N. X. N. )
17	14, 4, 16	wral 2814	. . 3 wff A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) )
18	17, 2, 16	crab 2818	. 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 1379	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  9300  0nnq  9301  elpqn  9302  pinq  9304  nqereu  9306