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	⊢ Q = { 𝑥 ∈ ( N × N ) ∣ ∀ 𝑦 ∈ ( N × N ) ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnq	⊢ Q
1		vx	⊢ 𝑥
2		cnpi	⊢ N
3	2 2	cxp	⊢ ( N × N )
4		vy	⊢ 𝑦
5	1	cv	⊢ 𝑥
6		ceq	⊢ ~Q
7	4	cv	⊢ 𝑦
8	5 7 6	wbr	⊢ 𝑥 ~Q 𝑦
9		c2nd	⊢ 2nd
10	7 9	cfv	⊢ ( 2nd ‘ 𝑦 )
11		clti	⊢ <N
12	5 9	cfv	⊢ ( 2nd ‘ 𝑥 )
13	10 12 11	wbr	⊢ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 )
14	13	wn	⊢ ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 )
15	8 14	wi	⊢ ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) )
16	15 4 3	wral	⊢ ∀ 𝑦 ∈ ( N × N ) ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) )
17	16 1 3	crab	⊢ { 𝑥 ∈ ( N × N ) ∣ ∀ 𝑦 ∈ ( N × N ) ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) }
18	0 17	wceq	⊢ Q = { 𝑥 ∈ ( N × N ) ∣ ∀ 𝑦 ∈ ( N × N ) ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) }