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

Definition df-iltp 6452
 Description: Define ordering on positive reals. We define x
Assertion
Ref Expression
df-iltp <P = {⟨x, y⟩ ∣ ((x P y P) 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty)))}
Distinct variable group:   x,y,𝑞

Detailed syntax breakdown of Definition df-iltp
StepHypRef Expression
1 cltp 6279 . 2 class <P
2 vx . . . . . . 7 setvar x
32cv 1241 . . . . . 6 class x
4 cnp 6275 . . . . . 6 class P
53, 4wcel 1390 . . . . 5 wff x P
6 vy . . . . . . 7 setvar y
76cv 1241 . . . . . 6 class y
87, 4wcel 1390 . . . . 5 wff y P
95, 8wa 97 . . . 4 wff (x P y P)
10 vq . . . . . . . 8 setvar 𝑞
1110cv 1241 . . . . . . 7 class 𝑞
12 c2nd 5708 . . . . . . . 8 class 2nd
133, 12cfv 4845 . . . . . . 7 class (2ndx)
1411, 13wcel 1390 . . . . . 6 wff 𝑞 (2ndx)
15 c1st 5707 . . . . . . . 8 class 1st
167, 15cfv 4845 . . . . . . 7 class (1sty)
1711, 16wcel 1390 . . . . . 6 wff 𝑞 (1sty)
1814, 17wa 97 . . . . 5 wff (𝑞 (2ndx) 𝑞 (1sty))
19 cnq 6264 . . . . 5 class Q
2018, 10, 19wrex 2301 . . . 4 wff 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty))
219, 20wa 97 . . 3 wff ((x P y P) 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty)))
2221, 2, 6copab 3808 . 2 class {⟨x, y⟩ ∣ ((x P y P) 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty)))}
231, 22wceq 1242 1 wff <P = {⟨x, y⟩ ∣ ((x P y P) 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty)))}
 Colors of variables: wff set class This definition is referenced by:  ltrelpr  6487  ltdfpr  6488
 Copyright terms: Public domain W3C validator