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

Definition df-iltp 7246
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
StepHypRef Expression
1 cltp 7071 . 2 class <P
2 vx . . . . . . 7 setvar 𝑥
32cv 1315 . . . . . 6 class 𝑥
4 cnp 7067 . . . . . 6 class P
53, 4wcel 1465 . . . . 5 wff 𝑥P
6 vy . . . . . . 7 setvar 𝑦
76cv 1315 . . . . . 6 class 𝑦
87, 4wcel 1465 . . . . 5 wff 𝑦P
95, 8wa 103 . . . 4 wff (𝑥P𝑦P)
10 vq . . . . . . . 8 setvar 𝑞
1110cv 1315 . . . . . . 7 class 𝑞
12 c2nd 6005 . . . . . . . 8 class 2nd
133, 12cfv 5093 . . . . . . 7 class (2nd𝑥)
1411, 13wcel 1465 . . . . . 6 wff 𝑞 ∈ (2nd𝑥)
15 c1st 6004 . . . . . . . 8 class 1st
167, 15cfv 5093 . . . . . . 7 class (1st𝑦)
1711, 16wcel 1465 . . . . . 6 wff 𝑞 ∈ (1st𝑦)
1814, 17wa 103 . . . . 5 wff (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))
19 cnq 7056 . . . . 5 class Q
2018, 10, 19wrex 2394 . . . 4 wff 𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))
219, 20wa 103 . . 3 wff ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))
2221, 2, 6copab 3958 . 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))}
231, 22wceq 1316 1 wff <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))}
Colors of variables: wff set class
This definition is referenced by:  ltrelpr  7281  ltdfpr  7282
  Copyright terms: Public domain W3C validator