Detailed syntax breakdown of Definition df-prob
Step | Hyp | Ref
| Expression |
1 | | cprb 32370 |
. 2
class
Prob |
2 | | vp |
. . . . . . . 8
setvar 𝑝 |
3 | 2 | cv 1541 |
. . . . . . 7
class 𝑝 |
4 | 3 | cdm 5590 |
. . . . . 6
class dom 𝑝 |
5 | 4 | cuni 4845 |
. . . . 5
class ∪ dom 𝑝 |
6 | 5, 3 | cfv 6432 |
. . . 4
class (𝑝‘∪ dom 𝑝) |
7 | | c1 10873 |
. . . 4
class
1 |
8 | 6, 7 | wceq 1542 |
. . 3
wff (𝑝‘∪ dom 𝑝) = 1 |
9 | | cmeas 32159 |
. . . . 5
class
measures |
10 | 9 | crn 5591 |
. . . 4
class ran
measures |
11 | 10 | cuni 4845 |
. . 3
class ∪ ran measures |
12 | 8, 2, 11 | crab 3070 |
. 2
class {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1} |
13 | 1, 12 | wceq 1542 |
1
wff Prob =
{𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1} |