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