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