Detailed syntax breakdown of Definition df-tmd
| Step | Hyp | Ref
| Expression |
| 1 | | ctmd 24078 |
. 2
class
TopMnd |
| 2 | | vf |
. . . . . . 7
setvar 𝑓 |
| 3 | 2 | cv 1539 |
. . . . . 6
class 𝑓 |
| 4 | | cplusf 18650 |
. . . . . 6
class
+𝑓 |
| 5 | 3, 4 | cfv 6561 |
. . . . 5
class
(+𝑓‘𝑓) |
| 6 | | vj |
. . . . . . . 8
setvar 𝑗 |
| 7 | 6 | cv 1539 |
. . . . . . 7
class 𝑗 |
| 8 | | ctx 23568 |
. . . . . . 7
class
×t |
| 9 | 7, 7, 8 | co 7431 |
. . . . . 6
class (𝑗 ×t 𝑗) |
| 10 | | ccn 23232 |
. . . . . 6
class
Cn |
| 11 | 9, 7, 10 | co 7431 |
. . . . 5
class ((𝑗 ×t 𝑗) Cn 𝑗) |
| 12 | 5, 11 | wcel 2108 |
. . . 4
wff
(+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗) |
| 13 | | ctopn 17466 |
. . . . 5
class
TopOpen |
| 14 | 3, 13 | cfv 6561 |
. . . 4
class
(TopOpen‘𝑓) |
| 15 | 12, 6, 14 | wsbc 3788 |
. . 3
wff
[(TopOpen‘𝑓) / 𝑗](+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗) |
| 16 | | cmnd 18747 |
. . . 4
class
Mnd |
| 17 | | ctps 22938 |
. . . 4
class
TopSp |
| 18 | 16, 17 | cin 3950 |
. . 3
class (Mnd
∩ TopSp) |
| 19 | 15, 2, 18 | crab 3436 |
. 2
class {𝑓 ∈ (Mnd ∩ TopSp)
∣ [(TopOpen‘𝑓) / 𝑗](+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗)} |
| 20 | 1, 19 | wceq 1540 |
1
wff TopMnd =
{𝑓 ∈ (Mnd ∩ TopSp)
∣ [(TopOpen‘𝑓) / 𝑗](+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗)} |