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	$⊢ 𝑸 = \{x \in (𝑵 \times 𝑵) \| \forall y \in (𝑵 \times 𝑵) (x ~_{𝑸} y \to \neg 2^{nd} (y) <_{𝑵} 2^{nd} (x))\}$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-nq

Detailed syntax breakdown