Detailed syntax breakdown of Definition df-sitm
Step | Hyp | Ref
| Expression |
1 | | csitm 32007 |
. 2
class
sitm |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | vm |
. . 3
setvar 𝑚 |
4 | | cvv 3408 |
. . 3
class
V |
5 | | cmeas 31875 |
. . . . 5
class
measures |
6 | 5 | crn 5552 |
. . . 4
class ran
measures |
7 | 6 | cuni 4819 |
. . 3
class ∪ ran measures |
8 | | vf |
. . . 4
setvar 𝑓 |
9 | | vg |
. . . 4
setvar 𝑔 |
10 | 2 | cv 1542 |
. . . . . 6
class 𝑤 |
11 | 3 | cv 1542 |
. . . . . 6
class 𝑚 |
12 | | csitg 32008 |
. . . . . 6
class
sitg |
13 | 10, 11, 12 | co 7213 |
. . . . 5
class (𝑤sitg𝑚) |
14 | 13 | cdm 5551 |
. . . 4
class dom
(𝑤sitg𝑚) |
15 | 8 | cv 1542 |
. . . . . 6
class 𝑓 |
16 | 9 | cv 1542 |
. . . . . 6
class 𝑔 |
17 | | cds 16811 |
. . . . . . . 8
class
dist |
18 | 10, 17 | cfv 6380 |
. . . . . . 7
class
(dist‘𝑤) |
19 | 18 | cof 7467 |
. . . . . 6
class
∘f (dist‘𝑤) |
20 | 15, 16, 19 | co 7213 |
. . . . 5
class (𝑓 ∘f
(dist‘𝑤)𝑔) |
21 | | cxrs 17005 |
. . . . . . 7
class
ℝ*𝑠 |
22 | | cc0 10729 |
. . . . . . . 8
class
0 |
23 | | cpnf 10864 |
. . . . . . . 8
class
+∞ |
24 | | cicc 12938 |
. . . . . . . 8
class
[,] |
25 | 22, 23, 24 | co 7213 |
. . . . . . 7
class
(0[,]+∞) |
26 | | cress 16784 |
. . . . . . 7
class
↾s |
27 | 21, 25, 26 | co 7213 |
. . . . . 6
class
(ℝ*𝑠 ↾s
(0[,]+∞)) |
28 | 27, 11, 12 | co 7213 |
. . . . 5
class
((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚) |
29 | 20, 28 | cfv 6380 |
. . . 4
class
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔)) |
30 | 8, 9, 14, 14, 29 | cmpo 7215 |
. . 3
class (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔))) |
31 | 2, 3, 4, 7, 30 | cmpo 7215 |
. 2
class (𝑤 ∈ V, 𝑚 ∈ ∪ ran
measures ↦ (𝑓 ∈
dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔)))) |
32 | 1, 31 | wceq 1543 |
1
wff sitm =
(𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔)))) |