Detailed syntax breakdown of Definition df-tlm
Step | Hyp | Ref
| Expression |
1 | | ctlm 23461 |
. 2
class
TopMod |
2 | | vw |
. . . . . . 7
setvar 𝑤 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑤 |
4 | | csca 17096 |
. . . . . 6
class
Scalar |
5 | 3, 4 | cfv 6494 |
. . . . 5
class
(Scalar‘𝑤) |
6 | | ctrg 23459 |
. . . . 5
class
TopRing |
7 | 5, 6 | wcel 2107 |
. . . 4
wff
(Scalar‘𝑤)
∈ TopRing |
8 | | cscaf 20276 |
. . . . . 6
class
·sf |
9 | 3, 8 | cfv 6494 |
. . . . 5
class (
·sf ‘𝑤) |
10 | | ctopn 17263 |
. . . . . . . 8
class
TopOpen |
11 | 5, 10 | cfv 6494 |
. . . . . . 7
class
(TopOpen‘(Scalar‘𝑤)) |
12 | 3, 10 | cfv 6494 |
. . . . . . 7
class
(TopOpen‘𝑤) |
13 | | ctx 22863 |
. . . . . . 7
class
×t |
14 | 11, 12, 13 | co 7352 |
. . . . . 6
class
((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) |
15 | | ccn 22527 |
. . . . . 6
class
Cn |
16 | 14, 12, 15 | co 7352 |
. . . . 5
class
(((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤)) |
17 | 9, 16 | wcel 2107 |
. . . 4
wff (
·sf ‘𝑤) ∈ (((TopOpen‘(Scalar‘𝑤)) ×t
(TopOpen‘𝑤)) Cn
(TopOpen‘𝑤)) |
18 | 7, 17 | wa 397 |
. . 3
wff
((Scalar‘𝑤)
∈ TopRing ∧ ( ·sf ‘𝑤) ∈
(((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤))) |
19 | | ctmd 23373 |
. . . 4
class
TopMnd |
20 | | clmod 20275 |
. . . 4
class
LMod |
21 | 19, 20 | cin 3908 |
. . 3
class (TopMnd
∩ LMod) |
22 | 18, 2, 21 | crab 3406 |
. 2
class {𝑤 ∈ (TopMnd ∩ LMod)
∣ ((Scalar‘𝑤)
∈ TopRing ∧ ( ·sf ‘𝑤) ∈
(((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤)))} |
23 | 1, 22 | wceq 1542 |
1
wff TopMod =
{𝑤 ∈ (TopMnd ∩
LMod) ∣ ((Scalar‘𝑤) ∈ TopRing ∧ (
·sf ‘𝑤) ∈ (((TopOpen‘(Scalar‘𝑤)) ×t
(TopOpen‘𝑤)) Cn
(TopOpen‘𝑤)))} |