Detailed syntax breakdown of Definition df-sitg
Step | Hyp | Ref
| Expression |
1 | | csitg 31866 |
. 2
class
sitg |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | vm |
. . 3
setvar 𝑚 |
4 | | cvv 3398 |
. . 3
class
V |
5 | | cmeas 31733 |
. . . . 5
class
measures |
6 | 5 | crn 5526 |
. . . 4
class ran
measures |
7 | 6 | cuni 4796 |
. . 3
class ∪ ran measures |
8 | | vf |
. . . 4
setvar 𝑓 |
9 | | vg |
. . . . . . . . 9
setvar 𝑔 |
10 | 9 | cv 1541 |
. . . . . . . 8
class 𝑔 |
11 | 10 | crn 5526 |
. . . . . . 7
class ran 𝑔 |
12 | | cfn 8555 |
. . . . . . 7
class
Fin |
13 | 11, 12 | wcel 2114 |
. . . . . 6
wff ran 𝑔 ∈ Fin |
14 | 10 | ccnv 5524 |
. . . . . . . . . 10
class ◡𝑔 |
15 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
16 | 15 | cv 1541 |
. . . . . . . . . . 11
class 𝑥 |
17 | 16 | csn 4516 |
. . . . . . . . . 10
class {𝑥} |
18 | 14, 17 | cima 5528 |
. . . . . . . . 9
class (◡𝑔 “ {𝑥}) |
19 | 3 | cv 1541 |
. . . . . . . . 9
class 𝑚 |
20 | 18, 19 | cfv 6339 |
. . . . . . . 8
class (𝑚‘(◡𝑔 “ {𝑥})) |
21 | | cc0 10615 |
. . . . . . . . 9
class
0 |
22 | | cpnf 10750 |
. . . . . . . . 9
class
+∞ |
23 | | cico 12823 |
. . . . . . . . 9
class
[,) |
24 | 21, 22, 23 | co 7170 |
. . . . . . . 8
class
(0[,)+∞) |
25 | 20, 24 | wcel 2114 |
. . . . . . 7
wff (𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) |
26 | 2 | cv 1541 |
. . . . . . . . . 10
class 𝑤 |
27 | | c0g 16816 |
. . . . . . . . . 10
class
0g |
28 | 26, 27 | cfv 6339 |
. . . . . . . . 9
class
(0g‘𝑤) |
29 | 28 | csn 4516 |
. . . . . . . 8
class
{(0g‘𝑤)} |
30 | 11, 29 | cdif 3840 |
. . . . . . 7
class (ran
𝑔 ∖
{(0g‘𝑤)}) |
31 | 25, 15, 30 | wral 3053 |
. . . . . 6
wff
∀𝑥 ∈
(ran 𝑔 ∖
{(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞) |
32 | 13, 31 | wa 399 |
. . . . 5
wff (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞)) |
33 | 19 | cdm 5525 |
. . . . . 6
class dom 𝑚 |
34 | | ctopn 16798 |
. . . . . . . 8
class
TopOpen |
35 | 26, 34 | cfv 6339 |
. . . . . . 7
class
(TopOpen‘𝑤) |
36 | | csigagen 31676 |
. . . . . . 7
class
sigaGen |
37 | 35, 36 | cfv 6339 |
. . . . . 6
class
(sigaGen‘(TopOpen‘𝑤)) |
38 | | cmbfm 31787 |
. . . . . 6
class
MblFnM |
39 | 33, 37, 38 | co 7170 |
. . . . 5
class (dom
𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) |
40 | 32, 9, 39 | crab 3057 |
. . . 4
class {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} |
41 | 8 | cv 1541 |
. . . . . . . 8
class 𝑓 |
42 | 41 | crn 5526 |
. . . . . . 7
class ran 𝑓 |
43 | 42, 29 | cdif 3840 |
. . . . . 6
class (ran
𝑓 ∖
{(0g‘𝑤)}) |
44 | 41 | ccnv 5524 |
. . . . . . . . . 10
class ◡𝑓 |
45 | 44, 17 | cima 5528 |
. . . . . . . . 9
class (◡𝑓 “ {𝑥}) |
46 | 45, 19 | cfv 6339 |
. . . . . . . 8
class (𝑚‘(◡𝑓 “ {𝑥})) |
47 | | csca 16671 |
. . . . . . . . . 10
class
Scalar |
48 | 26, 47 | cfv 6339 |
. . . . . . . . 9
class
(Scalar‘𝑤) |
49 | | crrh 31513 |
. . . . . . . . 9
class
ℝHom |
50 | 48, 49 | cfv 6339 |
. . . . . . . 8
class
(ℝHom‘(Scalar‘𝑤)) |
51 | 46, 50 | cfv 6339 |
. . . . . . 7
class
((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥}))) |
52 | | cvsca 16672 |
. . . . . . . 8
class
·𝑠 |
53 | 26, 52 | cfv 6339 |
. . . . . . 7
class (
·𝑠 ‘𝑤) |
54 | 51, 16, 53 | co 7170 |
. . . . . 6
class
(((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠
‘𝑤)𝑥) |
55 | 15, 43, 54 | cmpt 5110 |
. . . . 5
class (𝑥 ∈ (ran 𝑓 ∖ {(0g‘𝑤)}) ↦
(((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠
‘𝑤)𝑥)) |
56 | | cgsu 16817 |
. . . . 5
class
Σg |
57 | 26, 55, 56 | co 7170 |
. . . 4
class (𝑤 Σg
(𝑥 ∈ (ran 𝑓 ∖
{(0g‘𝑤)})
↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠
‘𝑤)𝑥))) |
58 | 8, 40, 57 | cmpt 5110 |
. . 3
class (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg
(𝑥 ∈ (ran 𝑓 ∖
{(0g‘𝑤)})
↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠
‘𝑤)𝑥)))) |
59 | 2, 3, 4, 7, 58 | cmpo 7172 |
. 2
class (𝑤 ∈ V, 𝑚 ∈ ∪ ran
measures ↦ (𝑓 ∈
{𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg
(𝑥 ∈ (ran 𝑓 ∖
{(0g‘𝑤)})
↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠
‘𝑤)𝑥))))) |
60 | 1, 59 | wceq 1542 |
1
wff sitg =
(𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g‘𝑤)})(𝑚‘(◡𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg
(𝑥 ∈ (ran 𝑓 ∖
{(0g‘𝑤)})
↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(◡𝑓 “ {𝑥})))( ·𝑠
‘𝑤)𝑥))))) |