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

Definition df-iltp 6568
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 6393 . 2 class <P
2 vx . . . . . . 7 setvar 𝑥
32cv 1242 . . . . . 6 class 𝑥
4 cnp 6389 . . . . . 6 class P
53, 4wcel 1393 . . . . 5 wff 𝑥P
6 vy . . . . . . 7 setvar 𝑦
76cv 1242 . . . . . 6 class 𝑦
87, 4wcel 1393 . . . . 5 wff 𝑦P
95, 8wa 97 . . . 4 wff (𝑥P𝑦P)
10 vq . . . . . . . 8 setvar 𝑞
1110cv 1242 . . . . . . 7 class 𝑞
12 c2nd 5766 . . . . . . . 8 class 2nd
133, 12cfv 4902 . . . . . . 7 class (2nd𝑥)
1411, 13wcel 1393 . . . . . 6 wff 𝑞 ∈ (2nd𝑥)
15 c1st 5765 . . . . . . . 8 class 1st
167, 15cfv 4902 . . . . . . 7 class (1st𝑦)
1711, 16wcel 1393 . . . . . 6 wff 𝑞 ∈ (1st𝑦)
1814, 17wa 97 . . . . 5 wff (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))
19 cnq 6378 . . . . 5 class Q
2018, 10, 19wrex 2307 . . . 4 wff 𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))
219, 20wa 97 . . 3 wff ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))
2221, 2, 6copab 3817 . 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))}
231, 22wceq 1243 1 wff <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))}
Colors of variables: wff set class
This definition is referenced by:  ltrelpr  6603  ltdfpr  6604
  Copyright terms: Public domain W3C validator