# 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 ${⊢}{\phi }\to {P}\in \mathrm{Prob}$
dstfrv.2 ${⊢}{\phi }\to {X}\in {\mathrm{RndVar}}_{ℝ}\left({P}\right)$
dstfrv.3 ${⊢}{\phi }\to {F}=\left({x}\in ℝ⟼{P}\left({X}{\le }_{\mathrm{RV/c}}{x}\right)\right)$
Assertion dstfrvclim1 ${⊢}{\phi }\to {F}⇝1$

### Proof

Step Hyp Ref Expression
1 dstfrv.1 ${⊢}{\phi }\to {P}\in \mathrm{Prob}$
2 dstfrv.2 ${⊢}{\phi }\to {X}\in {\mathrm{RndVar}}_{ℝ}\left({P}\right)$
3 dstfrv.3 ${⊢}{\phi }\to {F}=\left({x}\in ℝ⟼{P}\left({X}{\le }_{\mathrm{RV/c}}{x}\right)\right)$
4 eqid ${⊢}\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$
5 domprobmeas ${⊢}{P}\in \mathrm{Prob}\to {P}\in \mathrm{measures}\left(\mathrm{dom}{P}\right)$
6 1 5 syl ${⊢}{\phi }\to {P}\in \mathrm{measures}\left(\mathrm{dom}{P}\right)$
7 1 adantr ${⊢}\left({\phi }\wedge {i}\in ℕ\right)\to {P}\in \mathrm{Prob}$
8 2 adantr ${⊢}\left({\phi }\wedge {i}\in ℕ\right)\to {X}\in {\mathrm{RndVar}}_{ℝ}\left({P}\right)$
9 simpr ${⊢}\left({\phi }\wedge {i}\in ℕ\right)\to {i}\in ℕ$
10 9 nnred ${⊢}\left({\phi }\wedge {i}\in ℕ\right)\to {i}\in ℝ$
11 7 8 10 orvclteel ${⊢}\left({\phi }\wedge {i}\in ℕ\right)\to {X}{\le }_{\mathrm{RV/c}}{i}\in \mathrm{dom}{P}$
12 11 fmpttd ${⊢}{\phi }\to \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right):ℕ⟶\mathrm{dom}{P}$
13 1 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {P}\in \mathrm{Prob}$
14 2 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {X}\in {\mathrm{RndVar}}_{ℝ}\left({P}\right)$
15 simpr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℕ$
16 15 nnred ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℝ$
17 15 peano2nnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}+1\in ℕ$
18 17 nnred ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}+1\in ℝ$
19 16 lep1d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\le {n}+1$
20 13 14 16 18 19 orvclteinc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {X}{\le }_{\mathrm{RV/c}}{n}\subseteq {X}{\le }_{\mathrm{RV/c}}\left({n}+1\right)$
21 eqidd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)=\left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)$
22 simpr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}={n}\right)\to {i}={n}$
23 22 oveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}={n}\right)\to {X}{\le }_{\mathrm{RV/c}}{i}={X}{\le }_{\mathrm{RV/c}}{n}$
24 13 14 16 orvclteel ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {X}{\le }_{\mathrm{RV/c}}{n}\in \mathrm{dom}{P}$
25 21 23 15 24 fvmptd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\left({n}\right)={X}{\le }_{\mathrm{RV/c}}{n}$
26 simpr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}={n}+1\right)\to {i}={n}+1$
27 26 oveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}={n}+1\right)\to {X}{\le }_{\mathrm{RV/c}}{i}={X}{\le }_{\mathrm{RV/c}}\left({n}+1\right)$
28 13 14 18 orvclteel ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {X}{\le }_{\mathrm{RV/c}}\left({n}+1\right)\in \mathrm{dom}{P}$
29 21 27 17 28 fvmptd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\left({n}+1\right)={X}{\le }_{\mathrm{RV/c}}\left({n}+1\right)$
30 20 25 29 3sstr4d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\left({n}\right)\subseteq \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\left({n}+1\right)$
31 4 6 12 30 meascnbl
32 measfn ${⊢}{P}\in \mathrm{measures}\left(\mathrm{dom}{P}\right)\to {P}Fn\mathrm{dom}{P}$
33 dffn5 ${⊢}{P}Fn\mathrm{dom}{P}↔{P}=\left({a}\in \mathrm{dom}{P}⟼{P}\left({a}\right)\right)$
34 33 biimpi ${⊢}{P}Fn\mathrm{dom}{P}\to {P}=\left({a}\in \mathrm{dom}{P}⟼{P}\left({a}\right)\right)$
35 6 32 34 3syl ${⊢}{\phi }\to {P}=\left({a}\in \mathrm{dom}{P}⟼{P}\left({a}\right)\right)$
36 prob01 ${⊢}\left({P}\in \mathrm{Prob}\wedge {a}\in \mathrm{dom}{P}\right)\to {P}\left({a}\right)\in \left[0,1\right]$
37 1 36 sylan ${⊢}\left({\phi }\wedge {a}\in \mathrm{dom}{P}\right)\to {P}\left({a}\right)\in \left[0,1\right]$
38 35 37 fmpt3d ${⊢}{\phi }\to {P}:\mathrm{dom}{P}⟶\left[0,1\right]$
39 fco ${⊢}\left({P}:\mathrm{dom}{P}⟶\left[0,1\right]\wedge \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right):ℕ⟶\mathrm{dom}{P}\right)\to \left({P}\circ \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\right):ℕ⟶\left[0,1\right]$
40 38 12 39 syl2anc ${⊢}{\phi }\to \left({P}\circ \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\right):ℕ⟶\left[0,1\right]$
41 1 2 dstfrvunirn ${⊢}{\phi }\to \bigcup \mathrm{ran}\left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)=\bigcup \mathrm{dom}{P}$
42 1 unveldomd ${⊢}{\phi }\to \bigcup \mathrm{dom}{P}\in \mathrm{dom}{P}$
43 41 42 eqeltrd ${⊢}{\phi }\to \bigcup \mathrm{ran}\left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\in \mathrm{dom}{P}$
44 prob01 ${⊢}\left({P}\in \mathrm{Prob}\wedge \bigcup \mathrm{ran}\left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\in \mathrm{dom}{P}\right)\to {P}\left(\bigcup \mathrm{ran}\left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\right)\in \left[0,1\right]$
45 1 43 44 syl2anc ${⊢}{\phi }\to {P}\left(\bigcup \mathrm{ran}\left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\right)\in \left[0,1\right]$
46 0xr ${⊢}0\in {ℝ}^{*}$
47 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
48 0le0 ${⊢}0\le 0$
49 1re ${⊢}1\in ℝ$
50 ltpnf ${⊢}1\in ℝ\to 1<\mathrm{+\infty }$
51 49 50 ax-mp ${⊢}1<\mathrm{+\infty }$
52 iccssico ${⊢}\left(\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\wedge \left(0\le 0\wedge 1<\mathrm{+\infty }\right)\right)\to \left[0,1\right]\subseteq \left[0,\mathrm{+\infty }\right)$
53 46 47 48 51 52 mp4an ${⊢}\left[0,1\right]\subseteq \left[0,\mathrm{+\infty }\right)$
54 4 40 45 53 lmlimxrge0
55 31 54 mpbid ${⊢}{\phi }\to \left({P}\circ \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\right)⇝{P}\left(\bigcup \mathrm{ran}\left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\right)$
56 eqidd ${⊢}{\phi }\to \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)=\left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)$
57 fveq2 ${⊢}{a}={X}{\le }_{\mathrm{RV/c}}{i}\to {P}\left({a}\right)={P}\left({X}{\le }_{\mathrm{RV/c}}{i}\right)$
58 11 56 35 57 fmptco ${⊢}{\phi }\to {P}\circ \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)=\left({i}\in ℕ⟼{P}\left({X}{\le }_{\mathrm{RV/c}}{i}\right)\right)$
59 3 adantr ${⊢}\left({\phi }\wedge {i}\in ℕ\right)\to {F}=\left({x}\in ℝ⟼{P}\left({X}{\le }_{\mathrm{RV/c}}{x}\right)\right)$
60 simpr ${⊢}\left(\left({\phi }\wedge {i}\in ℕ\right)\wedge {x}={i}\right)\to {x}={i}$
61 60 oveq2d ${⊢}\left(\left({\phi }\wedge {i}\in ℕ\right)\wedge {x}={i}\right)\to {X}{\le }_{\mathrm{RV/c}}{x}={X}{\le }_{\mathrm{RV/c}}{i}$
62 61 fveq2d ${⊢}\left(\left({\phi }\wedge {i}\in ℕ\right)\wedge {x}={i}\right)\to {P}\left({X}{\le }_{\mathrm{RV/c}}{x}\right)={P}\left({X}{\le }_{\mathrm{RV/c}}{i}\right)$
63 7 11 probvalrnd ${⊢}\left({\phi }\wedge {i}\in ℕ\right)\to {P}\left({X}{\le }_{\mathrm{RV/c}}{i}\right)\in ℝ$
64 59 62 10 63 fvmptd ${⊢}\left({\phi }\wedge {i}\in ℕ\right)\to {F}\left({i}\right)={P}\left({X}{\le }_{\mathrm{RV/c}}{i}\right)$
65 64 mpteq2dva ${⊢}{\phi }\to \left({i}\in ℕ⟼{F}\left({i}\right)\right)=\left({i}\in ℕ⟼{P}\left({X}{\le }_{\mathrm{RV/c}}{i}\right)\right)$
66 58 65 eqtr4d ${⊢}{\phi }\to {P}\circ \left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)=\left({i}\in ℕ⟼{F}\left({i}\right)\right)$
67 41 fveq2d ${⊢}{\phi }\to {P}\left(\bigcup \mathrm{ran}\left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\right)={P}\left(\bigcup \mathrm{dom}{P}\right)$
68 probtot ${⊢}{P}\in \mathrm{Prob}\to {P}\left(\bigcup \mathrm{dom}{P}\right)=1$
69 1 68 syl ${⊢}{\phi }\to {P}\left(\bigcup \mathrm{dom}{P}\right)=1$
70 67 69 eqtrd ${⊢}{\phi }\to {P}\left(\bigcup \mathrm{ran}\left({i}\in ℕ⟼{X}{\le }_{\mathrm{RV/c}}{i}\right)\right)=1$
71 55 66 70 3brtr3d ${⊢}{\phi }\to \left({i}\in ℕ⟼{F}\left({i}\right)\right)⇝1$
72 1z ${⊢}1\in ℤ$
73 reex ${⊢}ℝ\in \mathrm{V}$
74 73 mptex ${⊢}\left({x}\in ℝ⟼{P}\left({X}{\le }_{\mathrm{RV/c}}{x}\right)\right)\in \mathrm{V}$
75 3 74 syl6eqel ${⊢}{\phi }\to {F}\in \mathrm{V}$
76 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
77 eqid ${⊢}\left({i}\in ℕ⟼{F}\left({i}\right)\right)=\left({i}\in ℕ⟼{F}\left({i}\right)\right)$
78 76 77 climmpt ${⊢}\left(1\in ℤ\wedge {F}\in \mathrm{V}\right)\to \left({F}⇝1↔\left({i}\in ℕ⟼{F}\left({i}\right)\right)⇝1\right)$
79 72 75 78 sylancr ${⊢}{\phi }\to \left({F}⇝1↔\left({i}\in ℕ⟼{F}\left({i}\right)\right)⇝1\right)$
80 71 79 mpbird ${⊢}{\phi }\to {F}⇝1$