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

Definition df-lt 6704
 Description: Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
Assertion
Ref Expression
df-lt < = {⟨x, y⟩ ∣ ((x y ℝ) zw((x = ⟨z, 0R y = ⟨w, 0R⟩) z <R w))}
Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Definition df-lt
StepHypRef Expression
1 cltrr 6695 . 2 class <
2 vx . . . . . . 7 setvar x
32cv 1241 . . . . . 6 class x
4 cr 6690 . . . . . 6 class
53, 4wcel 1390 . . . . 5 wff x
6 vy . . . . . . 7 setvar y
76cv 1241 . . . . . 6 class y
87, 4wcel 1390 . . . . 5 wff y
95, 8wa 97 . . . 4 wff (x y ℝ)
10 vz . . . . . . . . . . 11 setvar z
1110cv 1241 . . . . . . . . . 10 class z
12 c0r 6282 . . . . . . . . . 10 class 0R
1311, 12cop 3370 . . . . . . . . 9 class z, 0R
143, 13wceq 1242 . . . . . . . 8 wff x = ⟨z, 0R
15 vw . . . . . . . . . . 11 setvar w
1615cv 1241 . . . . . . . . . 10 class w
1716, 12cop 3370 . . . . . . . . 9 class w, 0R
187, 17wceq 1242 . . . . . . . 8 wff y = ⟨w, 0R
1914, 18wa 97 . . . . . . 7 wff (x = ⟨z, 0R y = ⟨w, 0R⟩)
20 cltr 6287 . . . . . . . 8 class <R
2111, 16, 20wbr 3755 . . . . . . 7 wff z <R w
2219, 21wa 97 . . . . . 6 wff ((x = ⟨z, 0R y = ⟨w, 0R⟩) z <R w)
2322, 15wex 1378 . . . . 5 wff w((x = ⟨z, 0R y = ⟨w, 0R⟩) z <R w)
2423, 10wex 1378 . . . 4 wff zw((x = ⟨z, 0R y = ⟨w, 0R⟩) z <R w)
259, 24wa 97 . . 3 wff ((x y ℝ) zw((x = ⟨z, 0R y = ⟨w, 0R⟩) z <R w))
2625, 2, 6copab 3808 . 2 class {⟨x, y⟩ ∣ ((x y ℝ) zw((x = ⟨z, 0R y = ⟨w, 0R⟩) z <R w))}
271, 26wceq 1242 1 wff < = {⟨x, y⟩ ∣ ((x y ℝ) zw((x = ⟨z, 0R y = ⟨w, 0R⟩) z <R w))}
 Colors of variables: wff set class This definition is referenced by:  ltrelre  6710  ltresr  6716
 Copyright terms: Public domain W3C validator