Metamath Proof Explorer

Theorem dstfrvclim1

Description: The limit of the cumulative distribution function is one. (Contributed by Thierry Arnoux, 12-Feb-2017) (Revised by Thierry Arnoux, 11-Jul-2017)

Ref Expression
Hypotheses dstfrv.1 
|- ( ph -> P e. Prob )
dstfrv.2 
|- ( ph -> X e. ( rRndVar ` P ) )
dstfrv.3 
|- ( ph -> F = ( x e. RR |-> ( P ` ( X oRVC <_ x ) ) ) )
Assertion dstfrvclim1 
|- ( ph -> F ~~> 1 )

Proof

Step Hyp Ref Expression
1 dstfrv.1 
 |-  ( ph -> P e. Prob )
2 dstfrv.2 
 |-  ( ph -> X e. ( rRndVar ` P ) )
3 dstfrv.3 
 |-  ( ph -> F = ( x e. RR |-> ( P ` ( X oRVC <_ x ) ) ) )
4 eqid 
 |-  ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
5 domprobmeas 
 |-  ( P e. Prob -> P e. ( measures ` dom P ) )
6 1 5 syl 
 |-  ( ph -> P e. ( measures ` dom P ) )
7 1 adantr 
 |-  ( ( ph /\ i e. NN ) -> P e. Prob )
8 2 adantr 
 |-  ( ( ph /\ i e. NN ) -> X e. ( rRndVar ` P ) )
9 simpr 
 |-  ( ( ph /\ i e. NN ) -> i e. NN )
10 9 nnred 
 |-  ( ( ph /\ i e. NN ) -> i e. RR )
11 7 8 10 orvclteel 
 |-  ( ( ph /\ i e. NN ) -> ( X oRVC <_ i ) e. dom P )
12 11 fmpttd 
 |-  ( ph -> ( i e. NN |-> ( X oRVC <_ i ) ) : NN --> dom P )
13 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> P e. Prob )
14 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. ( rRndVar ` P ) )
15 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
16 15 nnred 
 |-  ( ( ph /\ n e. NN ) -> n e. RR )
17 15 peano2nnd 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. NN )
18 17 nnred 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. RR )
19 16 lep1d 
 |-  ( ( ph /\ n e. NN ) -> n <_ ( n + 1 ) )
20 13 14 16 18 19 orvclteinc 
 |-  ( ( ph /\ n e. NN ) -> ( X oRVC <_ n ) C_ ( X oRVC <_ ( n + 1 ) ) )
21 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( i e. NN |-> ( X oRVC <_ i ) ) = ( i e. NN |-> ( X oRVC <_ i ) ) )
22 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ i = n ) -> i = n )
23 22 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ i = n ) -> ( X oRVC <_ i ) = ( X oRVC <_ n ) )
24 13 14 16 orvclteel 
 |-  ( ( ph /\ n e. NN ) -> ( X oRVC <_ n ) e. dom P )
25 21 23 15 24 fvmptd 
 |-  ( ( ph /\ n e. NN ) -> ( ( i e. NN |-> ( X oRVC <_ i ) ) ` n ) = ( X oRVC <_ n ) )
26 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ i = ( n + 1 ) ) -> i = ( n + 1 ) )
27 26 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ i = ( n + 1 ) ) -> ( X oRVC <_ i ) = ( X oRVC <_ ( n + 1 ) ) )
28 13 14 18 orvclteel 
 |-  ( ( ph /\ n e. NN ) -> ( X oRVC <_ ( n + 1 ) ) e. dom P )
29 21 27 17 28 fvmptd 
 |-  ( ( ph /\ n e. NN ) -> ( ( i e. NN |-> ( X oRVC <_ i ) ) ` ( n + 1 ) ) = ( X oRVC <_ ( n + 1 ) ) )
30 20 25 29 3sstr4d 
 |-  ( ( ph /\ n e. NN ) -> ( ( i e. NN |-> ( X oRVC <_ i ) ) ` n ) C_ ( ( i e. NN |-> ( X oRVC <_ i ) ) ` ( n + 1 ) ) )
31 4 6 12 30 meascnbl 
 |-  ( ph -> ( P o. ( i e. NN |-> ( X oRVC <_ i ) ) ) ( ~~>t ` ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) ) ( P ` U. ran ( i e. NN |-> ( X oRVC <_ i ) ) ) )
32 measfn 
 |-  ( P e. ( measures ` dom P ) -> P Fn dom P )
33 dffn5 
 |-  ( P Fn dom P <-> P = ( a e. dom P |-> ( P ` a ) ) )
34 33 biimpi 
 |-  ( P Fn dom P -> P = ( a e. dom P |-> ( P ` a ) ) )
35 6 32 34 3syl 
 |-  ( ph -> P = ( a e. dom P |-> ( P ` a ) ) )
36 prob01 
 |-  ( ( P e. Prob /\ a e. dom P ) -> ( P ` a ) e. ( 0 [,] 1 ) )
37 1 36 sylan 
 |-  ( ( ph /\ a e. dom P ) -> ( P ` a ) e. ( 0 [,] 1 ) )
38 35 37 fmpt3d 
 |-  ( ph -> P : dom P --> ( 0 [,] 1 ) )
39 fco 
 |-  ( ( P : dom P --> ( 0 [,] 1 ) /\ ( i e. NN |-> ( X oRVC <_ i ) ) : NN --> dom P ) -> ( P o. ( i e. NN |-> ( X oRVC <_ i ) ) ) : NN --> ( 0 [,] 1 ) )
40 38 12 39 syl2anc 
 |-  ( ph -> ( P o. ( i e. NN |-> ( X oRVC <_ i ) ) ) : NN --> ( 0 [,] 1 ) )
41 1 2 dstfrvunirn 
 |-  ( ph -> U. ran ( i e. NN |-> ( X oRVC <_ i ) ) = U. dom P )
42 1 unveldomd 
 |-  ( ph -> U. dom P e. dom P )
43 41 42 eqeltrd 
 |-  ( ph -> U. ran ( i e. NN |-> ( X oRVC <_ i ) ) e. dom P )
44 prob01 
 |-  ( ( P e. Prob /\ U. ran ( i e. NN |-> ( X oRVC <_ i ) ) e. dom P ) -> ( P ` U. ran ( i e. NN |-> ( X oRVC <_ i ) ) ) e. ( 0 [,] 1 ) )
45 1 43 44 syl2anc 
 |-  ( ph -> ( P ` U. ran ( i e. NN |-> ( X oRVC <_ i ) ) ) e. ( 0 [,] 1 ) )
46 0xr 
 |-  0 e. RR*
47 pnfxr 
 |-  +oo e. RR*
48 0le0 
 |-  0 <_ 0
49 1re 
 |-  1 e. RR
50 ltpnf 
 |-  ( 1 e. RR -> 1 < +oo )
51 49 50 ax-mp 
 |-  1 < +oo
52 iccssico 
 |-  ( ( ( 0 e. RR* /\ +oo e. RR* ) /\ ( 0 <_ 0 /\ 1 < +oo ) ) -> ( 0 [,] 1 ) C_ ( 0 [,) +oo ) )
53 46 47 48 51 52 mp4an 
 |-  ( 0 [,] 1 ) C_ ( 0 [,) +oo )
54 4 40 45 53 lmlimxrge0 
 |-  ( ph -> ( ( P o. ( i e. NN |-> ( X oRVC <_ i ) ) ) ( ~~>t ` ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) ) ( P ` U. ran ( i e. NN |-> ( X oRVC <_ i ) ) ) <-> ( P o. ( i e. NN |-> ( X oRVC <_ i ) ) ) ~~> ( P ` U. ran ( i e. NN |-> ( X oRVC <_ i ) ) ) ) )
55 31 54 mpbid 
 |-  ( ph -> ( P o. ( i e. NN |-> ( X oRVC <_ i ) ) ) ~~> ( P ` U. ran ( i e. NN |-> ( X oRVC <_ i ) ) ) )
56 eqidd 
 |-  ( ph -> ( i e. NN |-> ( X oRVC <_ i ) ) = ( i e. NN |-> ( X oRVC <_ i ) ) )
57 fveq2 
 |-  ( a = ( X oRVC <_ i ) -> ( P ` a ) = ( P ` ( X oRVC <_ i ) ) )
58 11 56 35 57 fmptco 
 |-  ( ph -> ( P o. ( i e. NN |-> ( X oRVC <_ i ) ) ) = ( i e. NN |-> ( P ` ( X oRVC <_ i ) ) ) )
59 3 adantr 
 |-  ( ( ph /\ i e. NN ) -> F = ( x e. RR |-> ( P ` ( X oRVC <_ x ) ) ) )
60 simpr 
 |-  ( ( ( ph /\ i e. NN ) /\ x = i ) -> x = i )
61 60 oveq2d 
 |-  ( ( ( ph /\ i e. NN ) /\ x = i ) -> ( X oRVC <_ x ) = ( X oRVC <_ i ) )
62 61 fveq2d 
 |-  ( ( ( ph /\ i e. NN ) /\ x = i ) -> ( P ` ( X oRVC <_ x ) ) = ( P ` ( X oRVC <_ i ) ) )
63 7 11 probvalrnd 
 |-  ( ( ph /\ i e. NN ) -> ( P ` ( X oRVC <_ i ) ) e. RR )
64 59 62 10 63 fvmptd 
 |-  ( ( ph /\ i e. NN ) -> ( F ` i ) = ( P ` ( X oRVC <_ i ) ) )
65 64 mpteq2dva 
 |-  ( ph -> ( i e. NN |-> ( F ` i ) ) = ( i e. NN |-> ( P ` ( X oRVC <_ i ) ) ) )
66 58 65 eqtr4d 
 |-  ( ph -> ( P o. ( i e. NN |-> ( X oRVC <_ i ) ) ) = ( i e. NN |-> ( F ` i ) ) )
67 41 fveq2d 
 |-  ( ph -> ( P ` U. ran ( i e. NN |-> ( X oRVC <_ i ) ) ) = ( P ` U. dom P ) )
68 probtot 
 |-  ( P e. Prob -> ( P ` U. dom P ) = 1 )
69 1 68 syl 
 |-  ( ph -> ( P ` U. dom P ) = 1 )
70 67 69 eqtrd 
 |-  ( ph -> ( P ` U. ran ( i e. NN |-> ( X oRVC <_ i ) ) ) = 1 )
71 55 66 70 3brtr3d 
 |-  ( ph -> ( i e. NN |-> ( F ` i ) ) ~~> 1 )
72 1z 
 |-  1 e. ZZ
73 reex 
 |-  RR e. _V
74 73 mptex 
 |-  ( x e. RR |-> ( P ` ( X oRVC <_ x ) ) ) e. _V
75 3 74 eqeltrdi 
 |-  ( ph -> F e. _V )
76 nnuz 
 |-  NN = ( ZZ>= ` 1 )
77 eqid 
 |-  ( i e. NN |-> ( F ` i ) ) = ( i e. NN |-> ( F ` i ) )
78 76 77 climmpt 
 |-  ( ( 1 e. ZZ /\ F e. _V ) -> ( F ~~> 1 <-> ( i e. NN |-> ( F ` i ) ) ~~> 1 ) )
79 72 75 78 sylancr 
 |-  ( ph -> ( F ~~> 1 <-> ( i e. NN |-> ( F ` i ) ) ~~> 1 ) )
80 71 79 mpbird 
 |-  ( ph -> F ~~> 1 )