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

Definition df-iltp 7373
 Description: Define ordering on positive reals. We define 𝑥
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 7198 . 2 class <P
2 vx . . . . . . 7 setvar 𝑥
32cv 1334 . . . . . 6 class 𝑥
4 cnp 7194 . . . . . 6 class P
53, 4wcel 2128 . . . . 5 wff 𝑥P
6 vy . . . . . . 7 setvar 𝑦
76cv 1334 . . . . . 6 class 𝑦
87, 4wcel 2128 . . . . 5 wff 𝑦P
95, 8wa 103 . . . 4 wff (𝑥P𝑦P)
10 vq . . . . . . . 8 setvar 𝑞
1110cv 1334 . . . . . . 7 class 𝑞
12 c2nd 6081 . . . . . . . 8 class 2nd
133, 12cfv 5167 . . . . . . 7 class (2nd𝑥)
1411, 13wcel 2128 . . . . . 6 wff 𝑞 ∈ (2nd𝑥)
15 c1st 6080 . . . . . . . 8 class 1st
167, 15cfv 5167 . . . . . . 7 class (1st𝑦)
1711, 16wcel 2128 . . . . . 6 wff 𝑞 ∈ (1st𝑦)
1814, 17wa 103 . . . . 5 wff (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))
19 cnq 7183 . . . . 5 class Q
2018, 10, 19wrex 2436 . . . 4 wff 𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦))
219, 20wa 103 . . 3 wff ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))
2221, 2, 6copab 4024 . 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))}
231, 22wceq 1335 1 wff <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ ∃𝑞Q (𝑞 ∈ (2nd𝑥) ∧ 𝑞 ∈ (1st𝑦)))}
 Colors of variables: wff set class This definition is referenced by:  ltrelpr  7408  ltdfpr  7409
 Copyright terms: Public domain W3C validator