Step | Hyp | Ref
| Expression |
1 | | csitg 32969 |
. 2
class
sitg |
2 | | vw |
. . 3
setvar π€ |
3 | | vm |
. . 3
setvar π |
4 | | cvv 3448 |
. . 3
class
V |
5 | | cmeas 32834 |
. . . . 5
class
measures |
6 | 5 | crn 5639 |
. . . 4
class ran
measures |
7 | 6 | cuni 4870 |
. . 3
class βͺ ran measures |
8 | | vf |
. . . 4
setvar π |
9 | | vg |
. . . . . . . . 9
setvar π |
10 | 9 | cv 1541 |
. . . . . . . 8
class π |
11 | 10 | crn 5639 |
. . . . . . 7
class ran π |
12 | | cfn 8890 |
. . . . . . 7
class
Fin |
13 | 11, 12 | wcel 2107 |
. . . . . 6
wff ran π β Fin |
14 | 10 | ccnv 5637 |
. . . . . . . . . 10
class β‘π |
15 | | vx |
. . . . . . . . . . . 12
setvar π₯ |
16 | 15 | cv 1541 |
. . . . . . . . . . 11
class π₯ |
17 | 16 | csn 4591 |
. . . . . . . . . 10
class {π₯} |
18 | 14, 17 | cima 5641 |
. . . . . . . . 9
class (β‘π β {π₯}) |
19 | 3 | cv 1541 |
. . . . . . . . 9
class π |
20 | 18, 19 | cfv 6501 |
. . . . . . . 8
class (πβ(β‘π β {π₯})) |
21 | | cc0 11058 |
. . . . . . . . 9
class
0 |
22 | | cpnf 11193 |
. . . . . . . . 9
class
+β |
23 | | cico 13273 |
. . . . . . . . 9
class
[,) |
24 | 21, 22, 23 | co 7362 |
. . . . . . . 8
class
(0[,)+β) |
25 | 20, 24 | wcel 2107 |
. . . . . . 7
wff (πβ(β‘π β {π₯})) β (0[,)+β) |
26 | 2 | cv 1541 |
. . . . . . . . . 10
class π€ |
27 | | c0g 17328 |
. . . . . . . . . 10
class
0g |
28 | 26, 27 | cfv 6501 |
. . . . . . . . 9
class
(0gβπ€) |
29 | 28 | csn 4591 |
. . . . . . . 8
class
{(0gβπ€)} |
30 | 11, 29 | cdif 3912 |
. . . . . . 7
class (ran
π β
{(0gβπ€)}) |
31 | 25, 15, 30 | wral 3065 |
. . . . . 6
wff
βπ₯ β
(ran π β
{(0gβπ€)})(πβ(β‘π β {π₯})) β (0[,)+β) |
32 | 13, 31 | wa 397 |
. . . . 5
wff (ran π β Fin β§ βπ₯ β (ran π β {(0gβπ€)})(πβ(β‘π β {π₯})) β (0[,)+β)) |
33 | 19 | cdm 5638 |
. . . . . 6
class dom π |
34 | | ctopn 17310 |
. . . . . . . 8
class
TopOpen |
35 | 26, 34 | cfv 6501 |
. . . . . . 7
class
(TopOpenβπ€) |
36 | | csigagen 32777 |
. . . . . . 7
class
sigaGen |
37 | 35, 36 | cfv 6501 |
. . . . . 6
class
(sigaGenβ(TopOpenβπ€)) |
38 | | cmbfm 32888 |
. . . . . 6
class
MblFnM |
39 | 33, 37, 38 | co 7362 |
. . . . 5
class (dom
πMblFnM(sigaGenβ(TopOpenβπ€))) |
40 | 32, 9, 39 | crab 3410 |
. . . 4
class {π β (dom πMblFnM(sigaGenβ(TopOpenβπ€))) β£ (ran π β Fin β§ βπ₯ β (ran π β {(0gβπ€)})(πβ(β‘π β {π₯})) β (0[,)+β))} |
41 | 8 | cv 1541 |
. . . . . . . 8
class π |
42 | 41 | crn 5639 |
. . . . . . 7
class ran π |
43 | 42, 29 | cdif 3912 |
. . . . . 6
class (ran
π β
{(0gβπ€)}) |
44 | 41 | ccnv 5637 |
. . . . . . . . . 10
class β‘π |
45 | 44, 17 | cima 5641 |
. . . . . . . . 9
class (β‘π β {π₯}) |
46 | 45, 19 | cfv 6501 |
. . . . . . . 8
class (πβ(β‘π β {π₯})) |
47 | | csca 17143 |
. . . . . . . . . 10
class
Scalar |
48 | 26, 47 | cfv 6501 |
. . . . . . . . 9
class
(Scalarβπ€) |
49 | | crrh 32614 |
. . . . . . . . 9
class
βHom |
50 | 48, 49 | cfv 6501 |
. . . . . . . 8
class
(βHomβ(Scalarβπ€)) |
51 | 46, 50 | cfv 6501 |
. . . . . . 7
class
((βHomβ(Scalarβπ€))β(πβ(β‘π β {π₯}))) |
52 | | cvsca 17144 |
. . . . . . . 8
class
Β·π |
53 | 26, 52 | cfv 6501 |
. . . . . . 7
class (
Β·π βπ€) |
54 | 51, 16, 53 | co 7362 |
. . . . . 6
class
(((βHomβ(Scalarβπ€))β(πβ(β‘π β {π₯})))( Β·π
βπ€)π₯) |
55 | 15, 43, 54 | cmpt 5193 |
. . . . 5
class (π₯ β (ran π β {(0gβπ€)}) β¦
(((βHomβ(Scalarβπ€))β(πβ(β‘π β {π₯})))( Β·π
βπ€)π₯)) |
56 | | cgsu 17329 |
. . . . 5
class
Ξ£g |
57 | 26, 55, 56 | co 7362 |
. . . 4
class (π€ Ξ£g
(π₯ β (ran π β
{(0gβπ€)})
β¦ (((βHomβ(Scalarβπ€))β(πβ(β‘π β {π₯})))( Β·π
βπ€)π₯))) |
58 | 8, 40, 57 | cmpt 5193 |
. . 3
class (π β {π β (dom πMblFnM(sigaGenβ(TopOpenβπ€))) β£ (ran π β Fin β§ βπ₯ β (ran π β {(0gβπ€)})(πβ(β‘π β {π₯})) β (0[,)+β))} β¦ (π€ Ξ£g
(π₯ β (ran π β
{(0gβπ€)})
β¦ (((βHomβ(Scalarβπ€))β(πβ(β‘π β {π₯})))( Β·π
βπ€)π₯)))) |
59 | 2, 3, 4, 7, 58 | cmpo 7364 |
. 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βπ€))β(πβ(β‘π β {π₯})))( Β·π
βπ€)π₯))))) |