df-ltpq

Description: Define pre-ordering relation on 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. Similar to Definition 5 of Suppes p. 162. (Contributed by NM, 28-Aug-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-ltpq	$⊢ <_{𝑝𝑸} = \{⟨x, y⟩ \| ((x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltpq	$class <_{𝑝𝑸}$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4		cnpi	$class 𝑵$
5	4 4	cxp	$class (𝑵 \times 𝑵)$
6	3 5	wcel	$wff x \in (𝑵 \times 𝑵)$
7	2	cv	$setvar y$
8	7 5	wcel	$wff y \in (𝑵 \times 𝑵)$
9	6 8	wa	$wff (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵))$
10		c1st	$class 1^{st}$
11	3 10	cfv	$class 1^{st} (x)$
12		cmi	$class \cdot_{𝑵}$
13		c2nd	$class 2^{nd}$
14	7 13	cfv	$class 2^{nd} (y)$
15	11 14 12	co	$class (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))$
16		clti	$class <_{𝑵}$
17	7 10	cfv	$class 1^{st} (y)$
18	3 13	cfv	$class 2^{nd} (x)$
19	17 18 12	co	$class (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))$
20	15 19 16	wbr	$wff (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))$
21	9 20	wa	$wff ((x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)))$
22	21 1 2	copab	$class \{⟨x, y⟩ \| ((x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)))\}$
23	0 22	wceq	$wff <_{𝑝𝑸} = \{⟨x, y⟩ \| ((x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)))\}$

Metamath Proof Explorer

Definition df-ltpq

Detailed syntax breakdown