Definition df-nq 9073

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 9280, 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 9011	. 2 class Q.
2		vx	. . . . . . 7 setvar x
3	2	cv 1368	. . . . . 6 class x
4		vy	. . . . . . 7 setvar y
5	4	cv 1368	. . . . . 6 class y
6		ceq 9010	. . . . . 6 class ~Q
7	3, 5, 6	wbr 4287	. . . . 5 wff x ~Q y
8		c2nd 6571	. . . . . . . 8 class 2nd
9	5, 8	cfv 5413	. . . . . . 7 class ( 2nd ` y )
10	3, 8	cfv 5413	. . . . . . 7 class ( 2nd ` x )
11		clti 9006	. . . . . . 7 class <N
12	9, 10, 11	wbr 4287	. . . . . 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 9003	. . . . 5 class N.
16	15, 15	cxp 4833	. . . 4 class ( N. X. N. )
17	14, 4, 16	wral 2710	. . 3 wff A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) )
18	17, 2, 16	crab 2714	. 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 1369	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  9084  0nnq  9085  elpqn  9086  pinq  9088  nqereu  9090