Metamath Proof Explorer

Theorem cndprob01

Description: The conditional probability has values in [ 0 , 1 ] . (Contributed by Thierry Arnoux, 13-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion cndprob01 
|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( ( cprob ` P ) ` <. A , B >. ) e. ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 cndprobval 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( ( cprob ` P ) ` <. A , B >. ) = ( ( P ` ( A i^i B ) ) / ( P ` B ) ) )
2 1 adantr 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( ( cprob ` P ) ` <. A , B >. ) = ( ( P ` ( A i^i B ) ) / ( P ` B ) ) )
3 simpl1 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> P e. Prob )
4 domprobmeas 
 |-  ( P e. Prob -> P e. ( measures ` dom P ) )
5 3 4 syl 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> P e. ( measures ` dom P ) )
6 domprobsiga 
 |-  ( P e. Prob -> dom P e. U. ran sigAlgebra )
7 3 6 syl 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> dom P e. U. ran sigAlgebra )
8 simpl2 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> A e. dom P )
9 simpl3 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> B e. dom P )
10 inelsiga 
 |-  ( ( dom P e. U. ran sigAlgebra /\ A e. dom P /\ B e. dom P ) -> ( A i^i B ) e. dom P )
11 7 8 9 10 syl3anc 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( A i^i B ) e. dom P )
12 inss2 
 |-  ( A i^i B ) C_ B
13 12 a1i 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( A i^i B ) C_ B )
14 5 11 9 13 measssd 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( P ` ( A i^i B ) ) <_ ( P ` B ) )
15 prob01 
 |-  ( ( P e. Prob /\ ( A i^i B ) e. dom P ) -> ( P ` ( A i^i B ) ) e. ( 0 [,] 1 ) )
16 3 11 15 syl2anc 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( P ` ( A i^i B ) ) e. ( 0 [,] 1 ) )
17 prob01 
 |-  ( ( P e. Prob /\ B e. dom P ) -> ( P ` B ) e. ( 0 [,] 1 ) )
18 3 9 17 syl2anc 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( P ` B ) e. ( 0 [,] 1 ) )
19 simpr 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( P ` B ) =/= 0 )
20 unitdivcld 
 |-  ( ( ( P ` ( A i^i B ) ) e. ( 0 [,] 1 ) /\ ( P ` B ) e. ( 0 [,] 1 ) /\ ( P ` B ) =/= 0 ) -> ( ( P ` ( A i^i B ) ) <_ ( P ` B ) <-> ( ( P ` ( A i^i B ) ) / ( P ` B ) ) e. ( 0 [,] 1 ) ) )
21 16 18 19 20 syl3anc 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( ( P ` ( A i^i B ) ) <_ ( P ` B ) <-> ( ( P ` ( A i^i B ) ) / ( P ` B ) ) e. ( 0 [,] 1 ) ) )
22 14 21 mpbid 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( ( P ` ( A i^i B ) ) / ( P ` B ) ) e. ( 0 [,] 1 ) )
23 2 22 eqeltrd 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( ( cprob ` P ) ` <. A , B >. ) e. ( 0 [,] 1 ) )