Definition df-nq 9195

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 9402, 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 9133	. 2 class Q.
2		vx	. . . . . . 7 setvar x
3	2	cv 1369	. . . . . 6 class x
4		vy	. . . . . . 7 setvar y
5	4	cv 1369	. . . . . 6 class y
6		ceq 9132	. . . . . 6 class ~Q
7	3, 5, 6	wbr 4403	. . . . 5 wff x ~Q y
8		c2nd 6689	. . . . . . . 8 class 2nd
9	5, 8	cfv 5529	. . . . . . 7 class ( 2nd ` y )
10	3, 8	cfv 5529	. . . . . . 7 class ( 2nd ` x )
11		clti 9128	. . . . . . 7 class <N
12	9, 10, 11	wbr 4403	. . . . . 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 9125	. . . . 5 class N.
16	15, 15	cxp 4949	. . . 4 class ( N. X. N. )
17	14, 4, 16	wral 2799	. . 3 wff A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) )
18	17, 2, 16	crab 2803	. 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 1370	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  9206  0nnq  9207  elpqn  9208  pinq  9210  nqereu  9212