Detailed syntax breakdown of Definition df-sitm
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | csitm 34331 | . 2
class
sitm | 
| 2 |  | vw | . . 3
setvar 𝑤 | 
| 3 |  | vm | . . 3
setvar 𝑚 | 
| 4 |  | cvv 3479 | . . 3
class
V | 
| 5 |  | cmeas 34197 | . . . . 5
class
measures | 
| 6 | 5 | crn 5685 | . . . 4
class ran
measures | 
| 7 | 6 | cuni 4906 | . . 3
class ∪ ran measures | 
| 8 |  | vf | . . . 4
setvar 𝑓 | 
| 9 |  | vg | . . . 4
setvar 𝑔 | 
| 10 | 2 | cv 1538 | . . . . . 6
class 𝑤 | 
| 11 | 3 | cv 1538 | . . . . . 6
class 𝑚 | 
| 12 |  | csitg 34332 | . . . . . 6
class
sitg | 
| 13 | 10, 11, 12 | co 7432 | . . . . 5
class (𝑤sitg𝑚) | 
| 14 | 13 | cdm 5684 | . . . 4
class dom
(𝑤sitg𝑚) | 
| 15 | 8 | cv 1538 | . . . . . 6
class 𝑓 | 
| 16 | 9 | cv 1538 | . . . . . 6
class 𝑔 | 
| 17 |  | cds 17307 | . . . . . . . 8
class
dist | 
| 18 | 10, 17 | cfv 6560 | . . . . . . 7
class
(dist‘𝑤) | 
| 19 | 18 | cof 7696 | . . . . . 6
class 
∘f (dist‘𝑤) | 
| 20 | 15, 16, 19 | co 7432 | . . . . 5
class (𝑓 ∘f
(dist‘𝑤)𝑔) | 
| 21 |  | cxrs 17546 | . . . . . . 7
class
ℝ*𝑠 | 
| 22 |  | cc0 11156 | . . . . . . . 8
class
0 | 
| 23 |  | cpnf 11293 | . . . . . . . 8
class
+∞ | 
| 24 |  | cicc 13391 | . . . . . . . 8
class
[,] | 
| 25 | 22, 23, 24 | co 7432 | . . . . . . 7
class
(0[,]+∞) | 
| 26 |  | cress 17275 | . . . . . . 7
class 
↾s | 
| 27 | 21, 25, 26 | co 7432 | . . . . . 6
class
(ℝ*𝑠 ↾s
(0[,]+∞)) | 
| 28 | 27, 11, 12 | co 7432 | . . . . 5
class
((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚) | 
| 29 | 20, 28 | cfv 6560 | . . . 4
class
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔)) | 
| 30 | 8, 9, 14, 14, 29 | cmpo 7434 | . . 3
class (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔))) | 
| 31 | 2, 3, 4, 7, 30 | cmpo 7434 | . 2
class (𝑤 ∈ V, 𝑚 ∈ ∪ ran
measures ↦ (𝑓 ∈
dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔)))) | 
| 32 | 1, 31 | wceq 1539 | 1
wff sitm =
(𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (𝑓 ∈ dom (𝑤sitg𝑚), 𝑔 ∈ dom (𝑤sitg𝑚) ↦
(((ℝ*𝑠 ↾s
(0[,]+∞))sitg𝑚)‘(𝑓 ∘f (dist‘𝑤)𝑔)))) |