Definition df-nq

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

	Ref	Expression
Assertion	df-nq	$$⊢𝑸=\left\{x\in \left(𝑵\times 𝑵\right)|\forall y\in \left(𝑵\times 𝑵\right)\left(x{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnq	$$class𝑸$$
1		vx	$$setvarx$$
2		cnpi	$$class𝑵$$
3	2 2	cxp	$$class\left(𝑵\times 𝑵\right)$$
4		vy	$$setvary$$
5	1	cv	$$setvarx$$
6		ceq	$$class{~}_{𝑸}$$
7	4	cv	$$setvary$$
8	5 7 6	wbr	$$wffx{~}_{𝑸}y$$
9		c2nd	$$class{2}^{nd}$$
10	7 9	cfv	$$class{2}^{nd}\left(y\right)$$
11		clti	$$class{<}_{𝑵}$$
12	5 9	cfv	$$class{2}^{nd}\left(x\right)$$
13	10 12 11	wbr	$$wff{2}^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)$$
14	13	wn	$$wff\neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)$$
15	8 14	wi	$$wff\left(x{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)\right)$$
16	15 4 3	wral	$$wff\forall y\in \left(𝑵\times 𝑵\right)\left(x{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)\right)$$
17	16 1 3	crab	$$class\left\{x\in \left(𝑵\times 𝑵\right)|\forall y\in \left(𝑵\times 𝑵\right)\left(x{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)\right)\right\}$$
18	0 17	wceq	$$wff𝑸=\left\{x\in \left(𝑵\times 𝑵\right)|\forall y\in \left(𝑵\times 𝑵\right)\left(x{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)\right)\right\}$$