Metamath Proof Explorer

Theorem prob01

Description: A probability is an element of [ 0 , 1 ]. First axiom of Kolmogorov. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion prob01 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → P ⁡ A ∈ 0 1

Proof

Step Hyp Ref Expression
1 domprobmeas ⊢ P ∈ Prob → P ∈ measures ⁡ dom ⁡ P
2 measvxrge0 ⊢ P ∈ measures ⁡ dom ⁡ P ∧ A ∈ dom ⁡ P → P ⁡ A ∈ 0 +∞
3 1 2 sylan ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → P ⁡ A ∈ 0 +∞
4 elxrge0 ⊢ P ⁡ A ∈ 0 +∞ ↔ P ⁡ A ∈ ℝ * ∧ 0 ≤ P ⁡ A
5 3 4 sylib ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → P ⁡ A ∈ ℝ * ∧ 0 ≤ P ⁡ A
6 1 adantr ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → P ∈ measures ⁡ dom ⁡ P
7 simpr ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → A ∈ dom ⁡ P
8 measbase ⊢ P ∈ measures ⁡ dom ⁡ P → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra
9 unielsiga ⊢ dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra → ⋃ dom ⁡ P ∈ dom ⁡ P
10 6 8 9 3syl ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → ⋃ dom ⁡ P ∈ dom ⁡ P
11 elssuni ⊢ A ∈ dom ⁡ P → A ⊆ ⋃ dom ⁡ P
12 11 adantl ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → A ⊆ ⋃ dom ⁡ P
13 6 7 10 12 measssd ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → P ⁡ A ≤ P ⁡ ⋃ dom ⁡ P
14 probtot ⊢ P ∈ Prob → P ⁡ ⋃ dom ⁡ P = 1
15 14 breq2d ⊢ P ∈ Prob → P ⁡ A ≤ P ⁡ ⋃ dom ⁡ P ↔ P ⁡ A ≤ 1
16 15 adantr ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → P ⁡ A ≤ P ⁡ ⋃ dom ⁡ P ↔ P ⁡ A ≤ 1
17 13 16 mpbid ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → P ⁡ A ≤ 1
18 df-3an ⊢ P ⁡ A ∈ ℝ * ∧ 0 ≤ P ⁡ A ∧ P ⁡ A ≤ 1 ↔ P ⁡ A ∈ ℝ * ∧ 0 ≤ P ⁡ A ∧ P ⁡ A ≤ 1
19 5 17 18 sylanbrc ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → P ⁡ A ∈ ℝ * ∧ 0 ≤ P ⁡ A ∧ P ⁡ A ≤ 1
20 0xr ⊢ 0 ∈ ℝ *
21 1xr ⊢ 1 ∈ ℝ *
22 elicc1 ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ * → P ⁡ A ∈ 0 1 ↔ P ⁡ A ∈ ℝ * ∧ 0 ≤ P ⁡ A ∧ P ⁡ A ≤ 1
23 20 21 22 mp2an ⊢ P ⁡ A ∈ 0 1 ↔ P ⁡ A ∈ ℝ * ∧ 0 ≤ P ⁡ A ∧ P ⁡ A ≤ 1
24 19 23 sylibr ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → P ⁡ A ∈ 0 1