Detailed syntax breakdown of Definition df-bj-divc
Step | Hyp | Ref
| Expression |
1 | | cdivc 35437 |
. 2
class
∥ℂ |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1538 |
. . . . . 6
class 𝑥 |
4 | | vy |
. . . . . . 7
setvar 𝑦 |
5 | 4 | cv 1538 |
. . . . . 6
class 𝑦 |
6 | 3, 5 | cop 4567 |
. . . . 5
class
〈𝑥, 𝑦〉 |
7 | | cccbar 35386 |
. . . . . . 7
class
ℂ̅ |
8 | 7, 7 | cxp 5587 |
. . . . . 6
class
(ℂ̅ × ℂ̅) |
9 | | ccchat 35403 |
. . . . . . 7
class
ℂ̂ |
10 | 9, 9 | cxp 5587 |
. . . . . 6
class
(ℂ̂ × ℂ̂) |
11 | 8, 10 | cun 3885 |
. . . . 5
class
((ℂ̅ × ℂ̅) ∪ (ℂ̂ ×
ℂ̂)) |
12 | 6, 11 | wcel 2106 |
. . . 4
wff 〈𝑥, 𝑦〉 ∈ ((ℂ̅ ×
ℂ̅) ∪ (ℂ̂ × ℂ̂)) |
13 | | vn |
. . . . . . . 8
setvar 𝑛 |
14 | 13 | cv 1538 |
. . . . . . 7
class 𝑛 |
15 | | cmulc 35416 |
. . . . . . 7
class
·ℂ̅ |
16 | 14, 3, 15 | co 7275 |
. . . . . 6
class (𝑛 ·ℂ̅
𝑥) |
17 | 16, 5 | wceq 1539 |
. . . . 5
wff (𝑛 ·ℂ̅
𝑥) = 𝑦 |
18 | | czzbar 35433 |
. . . . . 6
class
ℤ̅ |
19 | | czzhat 35435 |
. . . . . 6
class
ℤ̂ |
20 | 18, 19 | cun 3885 |
. . . . 5
class
(ℤ̅ ∪ ℤ̂) |
21 | 17, 13, 20 | wrex 3065 |
. . . 4
wff
∃𝑛 ∈
(ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦 |
22 | 12, 21 | wa 396 |
. . 3
wff
(〈𝑥, 𝑦〉 ∈ ((ℂ̅
× ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧
∃𝑛 ∈
(ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦) |
23 | 22, 2, 4 | copab 5136 |
. 2
class
{〈𝑥, 𝑦〉 ∣ (〈𝑥, 𝑦〉 ∈ ((ℂ̅ ×
ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧
∃𝑛 ∈
(ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)} |
24 | 1, 23 | wceq 1539 |
1
wff
∥ℂ = {〈𝑥, 𝑦〉 ∣ (〈𝑥, 𝑦〉 ∈ ((ℂ̅ ×
ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧
∃𝑛 ∈
(ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)} |