Detailed syntax breakdown of Definition df-enq
Step | Hyp | Ref
| Expression |
1 | | ceq 10465 |
. 2
class
~Q |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1542 |
. . . . . 6
class 𝑥 |
4 | | cnpi 10458 |
. . . . . . 7
class
N |
5 | 4, 4 | cxp 5549 |
. . . . . 6
class
(N × N) |
6 | 3, 5 | wcel 2110 |
. . . . 5
wff 𝑥 ∈ (N ×
N) |
7 | | vy |
. . . . . . 7
setvar 𝑦 |
8 | 7 | cv 1542 |
. . . . . 6
class 𝑦 |
9 | 8, 5 | wcel 2110 |
. . . . 5
wff 𝑦 ∈ (N ×
N) |
10 | 6, 9 | wa 399 |
. . . 4
wff (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) |
11 | | vz |
. . . . . . . . . . . . 13
setvar 𝑧 |
12 | 11 | cv 1542 |
. . . . . . . . . . . 12
class 𝑧 |
13 | | vw |
. . . . . . . . . . . . 13
setvar 𝑤 |
14 | 13 | cv 1542 |
. . . . . . . . . . . 12
class 𝑤 |
15 | 12, 14 | cop 4547 |
. . . . . . . . . . 11
class
〈𝑧, 𝑤〉 |
16 | 3, 15 | wceq 1543 |
. . . . . . . . . 10
wff 𝑥 = 〈𝑧, 𝑤〉 |
17 | | vv |
. . . . . . . . . . . . 13
setvar 𝑣 |
18 | 17 | cv 1542 |
. . . . . . . . . . . 12
class 𝑣 |
19 | | vu |
. . . . . . . . . . . . 13
setvar 𝑢 |
20 | 19 | cv 1542 |
. . . . . . . . . . . 12
class 𝑢 |
21 | 18, 20 | cop 4547 |
. . . . . . . . . . 11
class
〈𝑣, 𝑢〉 |
22 | 8, 21 | wceq 1543 |
. . . . . . . . . 10
wff 𝑦 = 〈𝑣, 𝑢〉 |
23 | 16, 22 | wa 399 |
. . . . . . . . 9
wff (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) |
24 | | cmi 10460 |
. . . . . . . . . . 11
class
·N |
25 | 12, 20, 24 | co 7213 |
. . . . . . . . . 10
class (𝑧
·N 𝑢) |
26 | 14, 18, 24 | co 7213 |
. . . . . . . . . 10
class (𝑤
·N 𝑣) |
27 | 25, 26 | wceq 1543 |
. . . . . . . . 9
wff (𝑧
·N 𝑢) = (𝑤 ·N 𝑣) |
28 | 23, 27 | wa 399 |
. . . . . . . 8
wff ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)) |
29 | 28, 19 | wex 1787 |
. . . . . . 7
wff
∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)) |
30 | 29, 17 | wex 1787 |
. . . . . 6
wff
∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)) |
31 | 30, 13 | wex 1787 |
. . . . 5
wff
∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)) |
32 | 31, 11 | wex 1787 |
. . . 4
wff
∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)) |
33 | 10, 32 | wa 399 |
. . 3
wff ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣))) |
34 | 33, 2, 7 | copab 5115 |
. 2
class
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))} |
35 | 1, 34 | wceq 1543 |
1
wff
~Q = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))} |