Detailed syntax breakdown of Definition df-tmd
Step | Hyp | Ref
| Expression |
1 | | ctmd 24093 |
. 2
class
TopMnd |
2 | | vf |
. . . . . . 7
setvar 𝑓 |
3 | 2 | cv 1535 |
. . . . . 6
class 𝑓 |
4 | | cplusf 18662 |
. . . . . 6
class
+𝑓 |
5 | 3, 4 | cfv 6562 |
. . . . 5
class
(+𝑓‘𝑓) |
6 | | vj |
. . . . . . . 8
setvar 𝑗 |
7 | 6 | cv 1535 |
. . . . . . 7
class 𝑗 |
8 | | ctx 23583 |
. . . . . . 7
class
×t |
9 | 7, 7, 8 | co 7430 |
. . . . . 6
class (𝑗 ×t 𝑗) |
10 | | ccn 23247 |
. . . . . 6
class
Cn |
11 | 9, 7, 10 | co 7430 |
. . . . 5
class ((𝑗 ×t 𝑗) Cn 𝑗) |
12 | 5, 11 | wcel 2105 |
. . . 4
wff
(+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗) |
13 | | ctopn 17467 |
. . . . 5
class
TopOpen |
14 | 3, 13 | cfv 6562 |
. . . 4
class
(TopOpen‘𝑓) |
15 | 12, 6, 14 | wsbc 3790 |
. . 3
wff
[(TopOpen‘𝑓) / 𝑗](+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗) |
16 | | cmnd 18759 |
. . . 4
class
Mnd |
17 | | ctps 22953 |
. . . 4
class
TopSp |
18 | 16, 17 | cin 3961 |
. . 3
class (Mnd
∩ TopSp) |
19 | 15, 2, 18 | crab 3432 |
. 2
class {𝑓 ∈ (Mnd ∩ TopSp)
∣ [(TopOpen‘𝑓) / 𝑗](+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗)} |
20 | 1, 19 | wceq 1536 |
1
wff TopMnd =
{𝑓 ∈ (Mnd ∩ TopSp)
∣ [(TopOpen‘𝑓) / 𝑗](+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗)} |