Detailed syntax breakdown of Definition df-enq0
Step | Hyp | Ref
| Expression |
1 | | ceq0 7235 |
. 2
class
~Q0 |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1347 |
. . . . . 6
class 𝑥 |
4 | | com 4572 |
. . . . . . 7
class
ω |
5 | | cnpi 7221 |
. . . . . . 7
class
N |
6 | 4, 5 | cxp 4607 |
. . . . . 6
class (ω
× N) |
7 | 3, 6 | wcel 2141 |
. . . . 5
wff 𝑥 ∈ (ω ×
N) |
8 | | vy |
. . . . . . 7
setvar 𝑦 |
9 | 8 | cv 1347 |
. . . . . 6
class 𝑦 |
10 | 9, 6 | wcel 2141 |
. . . . 5
wff 𝑦 ∈ (ω ×
N) |
11 | 7, 10 | wa 103 |
. . . 4
wff (𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) |
12 | | vz |
. . . . . . . . . . . . 13
setvar 𝑧 |
13 | 12 | cv 1347 |
. . . . . . . . . . . 12
class 𝑧 |
14 | | vw |
. . . . . . . . . . . . 13
setvar 𝑤 |
15 | 14 | cv 1347 |
. . . . . . . . . . . 12
class 𝑤 |
16 | 13, 15 | cop 3584 |
. . . . . . . . . . 11
class
〈𝑧, 𝑤〉 |
17 | 3, 16 | wceq 1348 |
. . . . . . . . . 10
wff 𝑥 = 〈𝑧, 𝑤〉 |
18 | | vv |
. . . . . . . . . . . . 13
setvar 𝑣 |
19 | 18 | cv 1347 |
. . . . . . . . . . . 12
class 𝑣 |
20 | | vu |
. . . . . . . . . . . . 13
setvar 𝑢 |
21 | 20 | cv 1347 |
. . . . . . . . . . . 12
class 𝑢 |
22 | 19, 21 | cop 3584 |
. . . . . . . . . . 11
class
〈𝑣, 𝑢〉 |
23 | 9, 22 | wceq 1348 |
. . . . . . . . . 10
wff 𝑦 = 〈𝑣, 𝑢〉 |
24 | 17, 23 | wa 103 |
. . . . . . . . 9
wff (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) |
25 | | comu 6390 |
. . . . . . . . . . 11
class
·o |
26 | 13, 21, 25 | co 5850 |
. . . . . . . . . 10
class (𝑧 ·o 𝑢) |
27 | 15, 19, 25 | co 5850 |
. . . . . . . . . 10
class (𝑤 ·o 𝑣) |
28 | 26, 27 | wceq 1348 |
. . . . . . . . 9
wff (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣) |
29 | 24, 28 | wa 103 |
. . . . . . . 8
wff ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) |
30 | 29, 20 | wex 1485 |
. . . . . . 7
wff
∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) |
31 | 30, 18 | wex 1485 |
. . . . . 6
wff
∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) |
32 | 31, 14 | wex 1485 |
. . . . 5
wff
∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) |
33 | 32, 12 | wex 1485 |
. . . 4
wff
∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) |
34 | 11, 33 | wa 103 |
. . 3
wff ((𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
35 | 34, 2, 8 | copab 4047 |
. 2
class
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))} |
36 | 1, 35 | wceq 1348 |
1
wff
~Q0 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))} |