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 e. Prob /\ A e. dom P ) -> ( P ` A ) e. ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 domprobmeas 
 |-  ( P e. Prob -> P e. ( measures ` dom P ) )
2 measvxrge0 
 |-  ( ( P e. ( measures ` dom P ) /\ A e. dom P ) -> ( P ` A ) e. ( 0 [,] +oo ) )
3 1 2 sylan 
 |-  ( ( P e. Prob /\ A e. dom P ) -> ( P ` A ) e. ( 0 [,] +oo ) )
4 elxrge0 
 |-  ( ( P ` A ) e. ( 0 [,] +oo ) <-> ( ( P ` A ) e. RR* /\ 0 <_ ( P ` A ) ) )
5 3 4 sylib 
 |-  ( ( P e. Prob /\ A e. dom P ) -> ( ( P ` A ) e. RR* /\ 0 <_ ( P ` A ) ) )
6 1 adantr 
 |-  ( ( P e. Prob /\ A e. dom P ) -> P e. ( measures ` dom P ) )
7 simpr 
 |-  ( ( P e. Prob /\ A e. dom P ) -> A e. dom P )
8 measbase 
 |-  ( P e. ( measures ` dom P ) -> dom P e. U. ran sigAlgebra )
9 unielsiga 
 |-  ( dom P e. U. ran sigAlgebra -> U. dom P e. dom P )
10 6 8 9 3syl 
 |-  ( ( P e. Prob /\ A e. dom P ) -> U. dom P e. dom P )
11 elssuni 
 |-  ( A e. dom P -> A C_ U. dom P )
12 11 adantl 
 |-  ( ( P e. Prob /\ A e. dom P ) -> A C_ U. dom P )
13 6 7 10 12 measssd 
 |-  ( ( P e. Prob /\ A e. dom P ) -> ( P ` A ) <_ ( P ` U. dom P ) )
14 probtot 
 |-  ( P e. Prob -> ( P ` U. dom P ) = 1 )
15 14 breq2d 
 |-  ( P e. Prob -> ( ( P ` A ) <_ ( P ` U. dom P ) <-> ( P ` A ) <_ 1 ) )
16 15 adantr 
 |-  ( ( P e. Prob /\ A e. dom P ) -> ( ( P ` A ) <_ ( P ` U. dom P ) <-> ( P ` A ) <_ 1 ) )
17 13 16 mpbid 
 |-  ( ( P e. Prob /\ A e. dom P ) -> ( P ` A ) <_ 1 )
18 df-3an 
 |-  ( ( ( P ` A ) e. RR* /\ 0 <_ ( P ` A ) /\ ( P ` A ) <_ 1 ) <-> ( ( ( P ` A ) e. RR* /\ 0 <_ ( P ` A ) ) /\ ( P ` A ) <_ 1 ) )
19 5 17 18 sylanbrc 
 |-  ( ( P e. Prob /\ A e. dom P ) -> ( ( P ` A ) e. RR* /\ 0 <_ ( P ` A ) /\ ( P ` A ) <_ 1 ) )
20 0xr 
 |-  0 e. RR*
21 1xr 
 |-  1 e. RR*
22 elicc1 
 |-  ( ( 0 e. RR* /\ 1 e. RR* ) -> ( ( P ` A ) e. ( 0 [,] 1 ) <-> ( ( P ` A ) e. RR* /\ 0 <_ ( P ` A ) /\ ( P ` A ) <_ 1 ) ) )
23 20 21 22 mp2an 
 |-  ( ( P ` A ) e. ( 0 [,] 1 ) <-> ( ( P ` A ) e. RR* /\ 0 <_ ( P ` A ) /\ ( P ` A ) <_ 1 ) )
24 19 23 sylibr 
 |-  ( ( P e. Prob /\ A e. dom P ) -> ( P ` A ) e. ( 0 [,] 1 ) )