Definition df-iltp 7271

Description: Define ordering on positive reals. We define x <P y if there is a positive fraction q which is an element of the upper cut of x and the lower cut of y. From the definition of < in Section 11.2.1 of [HoTT], p. (varies).

This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 29-Sep-2019.)

Assertion

Ref	Expression
df-iltp	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }

Distinct variable group:   x, y, q

Detailed syntax breakdown of Definition df-iltp

Step	Hyp	Ref	Expression
1		cltp 7096	. 2 class <P
2		vx	. . . . . . 7 setvar x
3	2	cv 1330	. . . . . 6 class x
4		cnp 7092	. . . . . 6 class P.
5	3, 4	wcel 1480	. . . . 5 wff x e. P.
6		vy	. . . . . . 7 setvar y
7	6	cv 1330	. . . . . 6 class y
8	7, 4	wcel 1480	. . . . 5 wff y e. P.
9	5, 8	wa 103	. . . 4 wff ( x e. P. /\ y e. P. )
10		vq	. . . . . . . 8 setvar q
11	10	cv 1330	. . . . . . 7 class q
12		c2nd 6030	. . . . . . . 8 class 2nd
13	3, 12	cfv 5118	. . . . . . 7 class ( 2nd ` x )
14	11, 13	wcel 1480	. . . . . 6 wff q e. ( 2nd ` x )
15		c1st 6029	. . . . . . . 8 class 1st
16	7, 15	cfv 5118	. . . . . . 7 class ( 1st ` y )
17	11, 16	wcel 1480	. . . . . 6 wff q e. ( 1st ` y )
18	14, 17	wa 103	. . . . 5 wff ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) )
19		cnq 7081	. . . . 5 class Q.
20	18, 10, 19	wrex 2415	. . . 4 wff E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) )
21	9, 20	wa 103	. . 3 wff ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) )
22	21, 2, 6	copab 3983	. 2 class { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
23	1, 22	wceq 1331	1 wff <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }

This definition is referenced by:  ltrelpr  7306  ltdfpr  7307