Definition 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	⊢ <pQ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltpq	⊢ <pQ
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4		cnpi	⊢ N
5	4 4	cxp	⊢ ( N × N )
6	3 5	wcel	⊢ 𝑥 ∈ ( N × N )
7	2	cv	⊢ 𝑦
8	7 5	wcel	⊢ 𝑦 ∈ ( N × N )
9	6 8	wa	⊢ ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) )
10		c1st	⊢ 1st
11	3 10	cfv	⊢ ( 1st ‘ 𝑥 )
12		cmi	⊢ ·N
13		c2nd	⊢ 2nd
14	7 13	cfv	⊢ ( 2nd ‘ 𝑦 )
15	11 14 12	co	⊢ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) )
16		clti	⊢ <N
17	7 10	cfv	⊢ ( 1st ‘ 𝑦 )
18	3 13	cfv	⊢ ( 2nd ‘ 𝑥 )
19	17 18 12	co	⊢ ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) )
20	15 19 16	wbr	⊢ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) )
21	9 20	wa	⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) )
22	21 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) }
23	0 22	wceq	⊢ <pQ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) }