Description: The probability of the universe set is 1. Second axiom of Kolmogorov. (Contributed by Thierry Arnoux, 8-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | probtot | ⊢ ( 𝑃 ∈ Prob → ( 𝑃 ‘ ∪ dom 𝑃 ) = 1 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elprob | ⊢ ( 𝑃 ∈ Prob ↔ ( 𝑃 ∈ ∪ ran measures ∧ ( 𝑃 ‘ ∪ dom 𝑃 ) = 1 ) ) | |
2 | 1 | simprbi | ⊢ ( 𝑃 ∈ Prob → ( 𝑃 ‘ ∪ dom 𝑃 ) = 1 ) |