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

Definition df-ltnqqs 6337
 Description: Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 13-Feb-1996.)
Assertion
Ref Expression
df-ltnqqs <Q = {⟨x, y⟩ ∣ ((x Q y Q) zwvu((x = [⟨z, w⟩] ~Q y = [⟨v, u⟩] ~Q ) (z ·N u) <N (w ·N v)))}
Distinct variable group:   x,y,z,w,v,u

Detailed syntax breakdown of Definition df-ltnqqs
StepHypRef Expression
1 cltq 6269 . 2 class <Q
2 vx . . . . . . 7 setvar x
32cv 1241 . . . . . 6 class x
4 cnq 6264 . . . . . 6 class Q
53, 4wcel 1390 . . . . 5 wff x Q
6 vy . . . . . . 7 setvar y
76cv 1241 . . . . . 6 class y
87, 4wcel 1390 . . . . 5 wff y Q
95, 8wa 97 . . . 4 wff (x Q y Q)
10 vz . . . . . . . . . . . . . 14 setvar z
1110cv 1241 . . . . . . . . . . . . 13 class z
12 vw . . . . . . . . . . . . . 14 setvar w
1312cv 1241 . . . . . . . . . . . . 13 class w
1411, 13cop 3370 . . . . . . . . . . . 12 class z, w
15 ceq 6263 . . . . . . . . . . . 12 class ~Q
1614, 15cec 6040 . . . . . . . . . . 11 class [⟨z, w⟩] ~Q
173, 16wceq 1242 . . . . . . . . . 10 wff x = [⟨z, w⟩] ~Q
18 vv . . . . . . . . . . . . . 14 setvar v
1918cv 1241 . . . . . . . . . . . . 13 class v
20 vu . . . . . . . . . . . . . 14 setvar u
2120cv 1241 . . . . . . . . . . . . 13 class u
2219, 21cop 3370 . . . . . . . . . . . 12 class v, u
2322, 15cec 6040 . . . . . . . . . . 11 class [⟨v, u⟩] ~Q
247, 23wceq 1242 . . . . . . . . . 10 wff y = [⟨v, u⟩] ~Q
2517, 24wa 97 . . . . . . . . 9 wff (x = [⟨z, w⟩] ~Q y = [⟨v, u⟩] ~Q )
26 cmi 6258 . . . . . . . . . . 11 class ·N
2711, 21, 26co 5455 . . . . . . . . . 10 class (z ·N u)
2813, 19, 26co 5455 . . . . . . . . . 10 class (w ·N v)
29 clti 6259 . . . . . . . . . 10 class <N
3027, 28, 29wbr 3755 . . . . . . . . 9 wff (z ·N u) <N (w ·N v)
3125, 30wa 97 . . . . . . . 8 wff ((x = [⟨z, w⟩] ~Q y = [⟨v, u⟩] ~Q ) (z ·N u) <N (w ·N v))
3231, 20wex 1378 . . . . . . 7 wff u((x = [⟨z, w⟩] ~Q y = [⟨v, u⟩] ~Q ) (z ·N u) <N (w ·N v))
3332, 18wex 1378 . . . . . 6 wff vu((x = [⟨z, w⟩] ~Q y = [⟨v, u⟩] ~Q ) (z ·N u) <N (w ·N v))
3433, 12wex 1378 . . . . 5 wff wvu((x = [⟨z, w⟩] ~Q y = [⟨v, u⟩] ~Q ) (z ·N u) <N (w ·N v))
3534, 10wex 1378 . . . 4 wff zwvu((x = [⟨z, w⟩] ~Q y = [⟨v, u⟩] ~Q ) (z ·N u) <N (w ·N v))
369, 35wa 97 . . 3 wff ((x Q y Q) zwvu((x = [⟨z, w⟩] ~Q y = [⟨v, u⟩] ~Q ) (z ·N u) <N (w ·N v)))
3736, 2, 6copab 3808 . 2 class {⟨x, y⟩ ∣ ((x Q y Q) zwvu((x = [⟨z, w⟩] ~Q y = [⟨v, u⟩] ~Q ) (z ·N u) <N (w ·N v)))}
381, 37wceq 1242 1 wff <Q = {⟨x, y⟩ ∣ ((x Q y Q) zwvu((x = [⟨z, w⟩] ~Q y = [⟨v, u⟩] ~Q ) (z ·N u) <N (w ·N v)))}
 Colors of variables: wff set class This definition is referenced by:  ltrelnq  6349  ordpipqqs  6358
 Copyright terms: Public domain W3C validator