df-ltpq - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > df-ltpq		Unicode version

Definition df-ltpq 7308

Description: Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 28-Aug-1995.)

**Assertion**
Ref	Expression
df-ltpq	$/\$ $/\$

Distinct variable group:

**Detailed syntax breakdown of Definition df-ltpq**
Step	Hyp	Ref	Expression
1		cltpq 7240	. 2
2		vx	. . . . . . 7
3	2	cv 1347	. . . . . 6
4		cnpi 7234	. . . . . . 7
5	4, 4	cxp 4609	. . . . . 6
6	3, 5	wcel 2141	. . . . 5
7		vy	. . . . . . 7
8	7	cv 1347	. . . . . 6
9	8, 5	wcel 2141	. . . . 5
10	6, 9	wa 103	. . . 4 $/\$
11		c1st 6117	. . . . . . 7
12	3, 11	cfv 5198	. . . . . 6
13		c2nd 6118	. . . . . . 7
14	8, 13	cfv 5198	. . . . . 6
15		cmi 7236	. . . . . 6
16	12, 14, 15	co 5853	. . . . 5
17	8, 11	cfv 5198	. . . . . 6
18	3, 13	cfv 5198	. . . . . 6
19	17, 18, 15	co 5853	. . . . 5
20		clti 7237	. . . . 5
21	16, 19, 20	wbr 3989	. . . 4
22	10, 21	wa 103	. . 3 $/\$ $/\$
23	22, 2, 7	copab 4049	. 2 $/\$ $/\$
24	1, 23	wceq 1348	1 $/\$ $/\$

Colors of variables: wff set class

This definition is referenced by: (None)

W3C validator