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

Definition df-ltnqqs 7354
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 = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q โˆง ๐‘ฆ = [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q ) โˆง (๐‘ง ยทN ๐‘ข) <N (๐‘ค ยทN ๐‘ฃ)))}
Distinct variable group:   ๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘ฃ,๐‘ข

Detailed syntax breakdown of Definition df-ltnqqs
StepHypRef Expression
1 cltq 7286 . 2 class <Q
2 vx . . . . . . 7 setvar ๐‘ฅ
32cv 1352 . . . . . 6 class ๐‘ฅ
4 cnq 7281 . . . . . 6 class Q
53, 4wcel 2148 . . . . 5 wff ๐‘ฅ โˆˆ Q
6 vy . . . . . . 7 setvar ๐‘ฆ
76cv 1352 . . . . . 6 class ๐‘ฆ
87, 4wcel 2148 . . . . 5 wff ๐‘ฆ โˆˆ Q
95, 8wa 104 . . . 4 wff (๐‘ฅ โˆˆ Q โˆง ๐‘ฆ โˆˆ Q)
10 vz . . . . . . . . . . . . . 14 setvar ๐‘ง
1110cv 1352 . . . . . . . . . . . . 13 class ๐‘ง
12 vw . . . . . . . . . . . . . 14 setvar ๐‘ค
1312cv 1352 . . . . . . . . . . . . 13 class ๐‘ค
1411, 13cop 3597 . . . . . . . . . . . 12 class โŸจ๐‘ง, ๐‘คโŸฉ
15 ceq 7280 . . . . . . . . . . . 12 class ~Q
1614, 15cec 6535 . . . . . . . . . . 11 class [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q
173, 16wceq 1353 . . . . . . . . . 10 wff ๐‘ฅ = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q
18 vv . . . . . . . . . . . . . 14 setvar ๐‘ฃ
1918cv 1352 . . . . . . . . . . . . 13 class ๐‘ฃ
20 vu . . . . . . . . . . . . . 14 setvar ๐‘ข
2120cv 1352 . . . . . . . . . . . . 13 class ๐‘ข
2219, 21cop 3597 . . . . . . . . . . . 12 class โŸจ๐‘ฃ, ๐‘ขโŸฉ
2322, 15cec 6535 . . . . . . . . . . 11 class [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q
247, 23wceq 1353 . . . . . . . . . 10 wff ๐‘ฆ = [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q
2517, 24wa 104 . . . . . . . . 9 wff (๐‘ฅ = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q โˆง ๐‘ฆ = [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q )
26 cmi 7275 . . . . . . . . . . 11 class ยทN
2711, 21, 26co 5877 . . . . . . . . . 10 class (๐‘ง ยทN ๐‘ข)
2813, 19, 26co 5877 . . . . . . . . . 10 class (๐‘ค ยทN ๐‘ฃ)
29 clti 7276 . . . . . . . . . 10 class <N
3027, 28, 29wbr 4005 . . . . . . . . 9 wff (๐‘ง ยทN ๐‘ข) <N (๐‘ค ยทN ๐‘ฃ)
3125, 30wa 104 . . . . . . . 8 wff ((๐‘ฅ = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q โˆง ๐‘ฆ = [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q ) โˆง (๐‘ง ยทN ๐‘ข) <N (๐‘ค ยทN ๐‘ฃ))
3231, 20wex 1492 . . . . . . 7 wff โˆƒ๐‘ข((๐‘ฅ = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q โˆง ๐‘ฆ = [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q ) โˆง (๐‘ง ยทN ๐‘ข) <N (๐‘ค ยทN ๐‘ฃ))
3332, 18wex 1492 . . . . . 6 wff โˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q โˆง ๐‘ฆ = [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q ) โˆง (๐‘ง ยทN ๐‘ข) <N (๐‘ค ยทN ๐‘ฃ))
3433, 12wex 1492 . . . . 5 wff โˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q โˆง ๐‘ฆ = [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q ) โˆง (๐‘ง ยทN ๐‘ข) <N (๐‘ค ยทN ๐‘ฃ))
3534, 10wex 1492 . . . 4 wff โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q โˆง ๐‘ฆ = [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q ) โˆง (๐‘ง ยทN ๐‘ข) <N (๐‘ค ยทN ๐‘ฃ))
369, 35wa 104 . . 3 wff ((๐‘ฅ โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q โˆง ๐‘ฆ = [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q ) โˆง (๐‘ง ยทN ๐‘ข) <N (๐‘ค ยทN ๐‘ฃ)))
3736, 2, 6copab 4065 . 2 class {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q โˆง ๐‘ฆ = [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q ) โˆง (๐‘ง ยทN ๐‘ข) <N (๐‘ค ยทN ๐‘ฃ)))}
381, 37wceq 1353 1 wff <Q = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q โˆง ๐‘ฆ = [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q ) โˆง (๐‘ง ยทN ๐‘ข) <N (๐‘ค ยทN ๐‘ฃ)))}
Colors of variables: wff set class
This definition is referenced by:  ltrelnq  7366  ordpipqqs  7375
  Copyright terms: Public domain W3C validator