Step | Hyp | Ref
| Expression |
1 | | csitm 33327 |
. 2
class
sitm |
2 | | vw |
. . 3
setvar π€ |
3 | | vm |
. . 3
setvar π |
4 | | cvv 3475 |
. . 3
class
V |
5 | | cmeas 33193 |
. . . . 5
class
measures |
6 | 5 | crn 5678 |
. . . 4
class ran
measures |
7 | 6 | cuni 4909 |
. . 3
class βͺ ran measures |
8 | | vf |
. . . 4
setvar π |
9 | | vg |
. . . 4
setvar π |
10 | 2 | cv 1541 |
. . . . . 6
class π€ |
11 | 3 | cv 1541 |
. . . . . 6
class π |
12 | | csitg 33328 |
. . . . . 6
class
sitg |
13 | 10, 11, 12 | co 7409 |
. . . . 5
class (π€sitgπ) |
14 | 13 | cdm 5677 |
. . . 4
class dom
(π€sitgπ) |
15 | 8 | cv 1541 |
. . . . . 6
class π |
16 | 9 | cv 1541 |
. . . . . 6
class π |
17 | | cds 17206 |
. . . . . . . 8
class
dist |
18 | 10, 17 | cfv 6544 |
. . . . . . 7
class
(distβπ€) |
19 | 18 | cof 7668 |
. . . . . 6
class
βf (distβπ€) |
20 | 15, 16, 19 | co 7409 |
. . . . 5
class (π βf
(distβπ€)π) |
21 | | cxrs 17446 |
. . . . . . 7
class
β*π |
22 | | cc0 11110 |
. . . . . . . 8
class
0 |
23 | | cpnf 11245 |
. . . . . . . 8
class
+β |
24 | | cicc 13327 |
. . . . . . . 8
class
[,] |
25 | 22, 23, 24 | co 7409 |
. . . . . . 7
class
(0[,]+β) |
26 | | cress 17173 |
. . . . . . 7
class
βΎs |
27 | 21, 25, 26 | co 7409 |
. . . . . 6
class
(β*π βΎs
(0[,]+β)) |
28 | 27, 11, 12 | co 7409 |
. . . . 5
class
((β*π βΎs
(0[,]+β))sitgπ) |
29 | 20, 28 | cfv 6544 |
. . . 4
class
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf (distβπ€)π)) |
30 | 8, 9, 14, 14, 29 | cmpo 7411 |
. . 3
class (π β dom (π€sitgπ), π β dom (π€sitgπ) β¦
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf (distβπ€)π))) |
31 | 2, 3, 4, 7, 30 | cmpo 7411 |
. 2
class (π€ β V, π β βͺ ran
measures β¦ (π β
dom (π€sitgπ), π β dom (π€sitgπ) β¦
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf (distβπ€)π)))) |
32 | 1, 31 | wceq 1542 |
1
wff sitm =
(π€ β V, π β βͺ ran measures β¦ (π β dom (π€sitgπ), π β dom (π€sitgπ) β¦
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf (distβπ€)π)))) |