Definition df-iltp 7554

Description: Define ordering on positive reals. We define 𝑥<_P 𝑦 if there is a positive fraction 𝑞 which is an element of the upper cut of 𝑥 and the lower cut of 𝑦. 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 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)))}

Distinct variable group:   𝑥,𝑦,𝑞

Detailed syntax breakdown of Definition df-iltp

Step	Hyp	Ref	Expression
1		cltp 7379	. 2 class <P
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1363	. . . . . 6 class 𝑥
4		cnp 7375	. . . . . 6 class P
5	3, 4	wcel 2167	. . . . 5 wff 𝑥 ∈ P
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1363	. . . . . 6 class 𝑦
8	7, 4	wcel 2167	. . . . 5 wff 𝑦 ∈ P
9	5, 8	wa 104	. . . 4 wff (𝑥 ∈ P ∧ 𝑦 ∈ P)
10		vq	. . . . . . . 8 setvar 𝑞
11	10	cv 1363	. . . . . . 7 class 𝑞
12		c2nd 6206	. . . . . . . 8 class 2nd
13	3, 12	cfv 5259	. . . . . . 7 class (2nd ‘𝑥)
14	11, 13	wcel 2167	. . . . . 6 wff 𝑞 ∈ (2nd ‘𝑥)
15		c1st 6205	. . . . . . . 8 class 1st
16	7, 15	cfv 5259	. . . . . . 7 class (1st ‘𝑦)
17	11, 16	wcel 2167	. . . . . 6 wff 𝑞 ∈ (1st ‘𝑦)
18	14, 17	wa 104	. . . . 5 wff (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))
19		cnq 7364	. . . . 5 class Q
20	18, 10, 19	wrex 2476	. . . 4 wff ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))
21	9, 20	wa 104	. . 3 wff ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)))
22	21, 2, 6	copab 4094	. 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)))}
23	1, 22	wceq 1364	1 wff <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)))}

This definition is referenced by:  ltrelpr  7589  ltdfpr  7590