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 PProbAdomPPA01

Proof

Step Hyp Ref Expression
1 domprobmeas PProbPmeasuresdomP
2 measvxrge0 PmeasuresdomPAdomPPA0+∞
3 1 2 sylan PProbAdomPPA0+∞
4 elxrge0 PA0+∞PA*0PA
5 3 4 sylib PProbAdomPPA*0PA
6 1 adantr PProbAdomPPmeasuresdomP
7 simpr PProbAdomPAdomP
8 measbase PmeasuresdomPdomPransigAlgebra
9 unielsiga domPransigAlgebradomPdomP
10 6 8 9 3syl PProbAdomPdomPdomP
11 elssuni AdomPAdomP
12 11 adantl PProbAdomPAdomP
13 6 7 10 12 measssd PProbAdomPPAPdomP
14 probtot PProbPdomP=1
15 14 breq2d PProbPAPdomPPA1
16 15 adantr PProbAdomPPAPdomPPA1
17 13 16 mpbid PProbAdomPPA1
18 df-3an PA*0PAPA1PA*0PAPA1
19 5 17 18 sylanbrc PProbAdomPPA*0PAPA1
20 0xr 0*
21 1xr 1*
22 elicc1 0*1*PA01PA*0PAPA1
23 20 21 22 mp2an PA01PA*0PAPA1
24 19 23 sylibr PProbAdomPPA01