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 ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ( 𝑃𝐴 ) ∈ ( 0 [,] 1 ) )

Proof

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