Detailed syntax breakdown of Definition df-ltnqqs
Step | Hyp | Ref
| Expression |
1 | | cltq 6269 |
. 2
class
<Q |
2 | | vx |
. . . . . . 7
setvar x |
3 | 2 | cv 1241 |
. . . . . 6
class x |
4 | | cnq 6264 |
. . . . . 6
class
Q |
5 | 3, 4 | wcel 1390 |
. . . . 5
wff x ∈
Q |
6 | | vy |
. . . . . . 7
setvar y |
7 | 6 | cv 1241 |
. . . . . 6
class y |
8 | 7, 4 | wcel 1390 |
. . . . 5
wff y ∈
Q |
9 | 5, 8 | wa 97 |
. . . 4
wff (x ∈
Q ∧ y ∈
Q) |
10 | | vz |
. . . . . . . . . . . . . 14
setvar z |
11 | 10 | cv 1241 |
. . . . . . . . . . . . 13
class z |
12 | | vw |
. . . . . . . . . . . . . 14
setvar w |
13 | 12 | cv 1241 |
. . . . . . . . . . . . 13
class w |
14 | 11, 13 | cop 3370 |
. . . . . . . . . . . 12
class 〈z, w〉 |
15 | | ceq 6263 |
. . . . . . . . . . . 12
class
~Q |
16 | 14, 15 | cec 6040 |
. . . . . . . . . . 11
class [〈z, w〉]
~Q |
17 | 3, 16 | wceq 1242 |
. . . . . . . . . 10
wff x = [〈z,
w〉]
~Q |
18 | | vv |
. . . . . . . . . . . . . 14
setvar v |
19 | 18 | cv 1241 |
. . . . . . . . . . . . 13
class v |
20 | | vu |
. . . . . . . . . . . . . 14
setvar u |
21 | 20 | cv 1241 |
. . . . . . . . . . . . 13
class u |
22 | 19, 21 | cop 3370 |
. . . . . . . . . . . 12
class 〈v, u〉 |
23 | 22, 15 | cec 6040 |
. . . . . . . . . . 11
class [〈v, u〉]
~Q |
24 | 7, 23 | wceq 1242 |
. . . . . . . . . 10
wff y = [〈v,
u〉]
~Q |
25 | 17, 24 | wa 97 |
. . . . . . . . 9
wff (x = [〈z,
w〉] ~Q ∧ y =
[〈v, u〉] ~Q
) |
26 | | cmi 6258 |
. . . . . . . . . . 11
class
·N |
27 | 11, 21, 26 | co 5455 |
. . . . . . . . . 10
class (z ·N u) |
28 | 13, 19, 26 | co 5455 |
. . . . . . . . . 10
class (w ·N v) |
29 | | clti 6259 |
. . . . . . . . . 10
class
<N |
30 | 27, 28, 29 | wbr 3755 |
. . . . . . . . 9
wff (z ·N u) <N (w ·N v) |
31 | 25, 30 | wa 97 |
. . . . . . . 8
wff ((x = [〈z,
w〉] ~Q ∧ y =
[〈v, u〉] ~Q ) ∧ (z
·N u)
<N (w
·N v)) |
32 | 31, 20 | wex 1378 |
. . . . . . 7
wff ∃u((x = [〈z,
w〉] ~Q ∧ y =
[〈v, u〉] ~Q ) ∧ (z
·N u)
<N (w
·N v)) |
33 | 32, 18 | wex 1378 |
. . . . . 6
wff ∃v∃u((x = [〈z,
w〉] ~Q ∧ y =
[〈v, u〉] ~Q ) ∧ (z
·N u)
<N (w
·N v)) |
34 | 33, 12 | wex 1378 |
. . . . 5
wff ∃w∃v∃u((x = [〈z,
w〉] ~Q ∧ y =
[〈v, u〉] ~Q ) ∧ (z
·N u)
<N (w
·N v)) |
35 | 34, 10 | wex 1378 |
. . . 4
wff ∃z∃w∃v∃u((x = [〈z,
w〉] ~Q ∧ y =
[〈v, u〉] ~Q ) ∧ (z
·N u)
<N (w
·N v)) |
36 | 9, 35 | wa 97 |
. . 3
wff ((x ∈
Q ∧ y ∈
Q) ∧ ∃z∃w∃v∃u((x = [〈z,
w〉] ~Q ∧ y =
[〈v, u〉] ~Q ) ∧ (z
·N u)
<N (w
·N v))) |
37 | 36, 2, 6 | copab 3808 |
. 2
class {〈x, y〉
∣ ((x ∈ Q ∧ y ∈ Q) ∧ ∃z∃w∃v∃u((x =
[〈z, w〉] ~Q ∧ y =
[〈v, u〉] ~Q ) ∧ (z
·N u)
<N (w
·N v)))} |
38 | 1, 37 | wceq 1242 |
1
wff
<Q = {〈x,
y〉 ∣ ((x ∈
Q ∧ y ∈
Q) ∧ ∃z∃w∃v∃u((x = [〈z,
w〉] ~Q ∧ y =
[〈v, u〉] ~Q ) ∧ (z
·N u)
<N (w
·N v)))} |