Detailed syntax breakdown of Definition df-cnfld
| Step | Hyp | Ref
| Expression |
| 1 | | ccnfld 21364 |
. 2
class
ℂfld |
| 2 | | cnx 17230 |
. . . . . . 7
class
ndx |
| 3 | | cbs 17247 |
. . . . . . 7
class
Base |
| 4 | 2, 3 | cfv 6561 |
. . . . . 6
class
(Base‘ndx) |
| 5 | | cc 11153 |
. . . . . 6
class
ℂ |
| 6 | 4, 5 | cop 4632 |
. . . . 5
class
〈(Base‘ndx), ℂ〉 |
| 7 | | cplusg 17297 |
. . . . . . 7
class
+g |
| 8 | 2, 7 | cfv 6561 |
. . . . . 6
class
(+g‘ndx) |
| 9 | | vx |
. . . . . . 7
setvar 𝑥 |
| 10 | | vy |
. . . . . . 7
setvar 𝑦 |
| 11 | 9 | cv 1539 |
. . . . . . . 8
class 𝑥 |
| 12 | 10 | cv 1539 |
. . . . . . . 8
class 𝑦 |
| 13 | | caddc 11158 |
. . . . . . . 8
class
+ |
| 14 | 11, 12, 13 | co 7431 |
. . . . . . 7
class (𝑥 + 𝑦) |
| 15 | 9, 10, 5, 5, 14 | cmpo 7433 |
. . . . . 6
class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) |
| 16 | 8, 15 | cop 4632 |
. . . . 5
class
〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉 |
| 17 | | cmulr 17298 |
. . . . . . 7
class
.r |
| 18 | 2, 17 | cfv 6561 |
. . . . . 6
class
(.r‘ndx) |
| 19 | | cmul 11160 |
. . . . . . . 8
class
· |
| 20 | 11, 12, 19 | co 7431 |
. . . . . . 7
class (𝑥 · 𝑦) |
| 21 | 9, 10, 5, 5, 20 | cmpo 7433 |
. . . . . 6
class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) |
| 22 | 18, 21 | cop 4632 |
. . . . 5
class
〈(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉 |
| 23 | 6, 16, 22 | ctp 4630 |
. . . 4
class
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} |
| 24 | | cstv 17299 |
. . . . . . 7
class
*𝑟 |
| 25 | 2, 24 | cfv 6561 |
. . . . . 6
class
(*𝑟‘ndx) |
| 26 | | ccj 15135 |
. . . . . 6
class
∗ |
| 27 | 25, 26 | cop 4632 |
. . . . 5
class
〈(*𝑟‘ndx), ∗〉 |
| 28 | 27 | csn 4626 |
. . . 4
class
{〈(*𝑟‘ndx),
∗〉} |
| 29 | 23, 28 | cun 3949 |
. . 3
class
({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) |
| 30 | | cts 17303 |
. . . . . . 7
class
TopSet |
| 31 | 2, 30 | cfv 6561 |
. . . . . 6
class
(TopSet‘ndx) |
| 32 | | cabs 15273 |
. . . . . . . 8
class
abs |
| 33 | | cmin 11492 |
. . . . . . . 8
class
− |
| 34 | 32, 33 | ccom 5689 |
. . . . . . 7
class (abs
∘ − ) |
| 35 | | cmopn 21354 |
. . . . . . 7
class
MetOpen |
| 36 | 34, 35 | cfv 6561 |
. . . . . 6
class
(MetOpen‘(abs ∘ − )) |
| 37 | 31, 36 | cop 4632 |
. . . . 5
class
〈(TopSet‘ndx), (MetOpen‘(abs ∘ −
))〉 |
| 38 | | cple 17304 |
. . . . . . 7
class
le |
| 39 | 2, 38 | cfv 6561 |
. . . . . 6
class
(le‘ndx) |
| 40 | | cle 11296 |
. . . . . 6
class
≤ |
| 41 | 39, 40 | cop 4632 |
. . . . 5
class
〈(le‘ndx), ≤ 〉 |
| 42 | | cds 17306 |
. . . . . . 7
class
dist |
| 43 | 2, 42 | cfv 6561 |
. . . . . 6
class
(dist‘ndx) |
| 44 | 43, 34 | cop 4632 |
. . . . 5
class
〈(dist‘ndx), (abs ∘ − )〉 |
| 45 | 37, 41, 44 | ctp 4630 |
. . . 4
class
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} |
| 46 | | cunif 17307 |
. . . . . . 7
class
UnifSet |
| 47 | 2, 46 | cfv 6561 |
. . . . . 6
class
(UnifSet‘ndx) |
| 48 | | cmetu 21355 |
. . . . . . 7
class
metUnif |
| 49 | 34, 48 | cfv 6561 |
. . . . . 6
class
(metUnif‘(abs ∘ − )) |
| 50 | 47, 49 | cop 4632 |
. . . . 5
class
〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉 |
| 51 | 50 | csn 4626 |
. . . 4
class
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉} |
| 52 | 45, 51 | cun 3949 |
. . 3
class
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ −
))〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs
∘ − )〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs
∘ − ))〉}) |
| 53 | 29, 52 | cun 3949 |
. 2
class
(({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∪
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉})) |
| 54 | 1, 53 | wceq 1540 |
1
wff
ℂfld = (({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∪
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉})) |