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 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
dstfrv.2 ⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
dstfrv.3 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 ≤ 𝑥 ) ) ) )
Assertion dstfrvclim1 ( 𝜑 → 𝐹 ⇝ 1 )

Proof

Step Hyp Ref Expression
1 dstfrv.1 ⊢ ( 𝜑 → 𝑃 ∈ Prob )
2 dstfrv.2 ⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3 dstfrv.3 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 ≤ 𝑥 ) ) ) )
4 eqid ⊢ ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
5 domprobmeas ⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
6 1 5 syl ⊢ ( 𝜑 → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑃 ∈ Prob )
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
10 9 nnred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℝ )
11 7 8 10 orvclteel ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ∈ dom 𝑃 )
12 11 fmpttd ⊢ ( 𝜑 → ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) : ℕ ⟶ dom 𝑃 )
13 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ Prob )
14 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
16 15 nnred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ )
17 15 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℕ )
18 17 nnred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℝ )
19 16 lep1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ≤ ( 𝑛 + 1 ) )
20 13 14 16 18 19 orvclteinc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ⊆ ( 𝑋 ∘RV/𝑐 ≤ ( 𝑛 + 1 ) ) )
21 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) = ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) )
22 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 = 𝑛 ) → 𝑖 = 𝑛 )
23 22 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 = 𝑛 ) → ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) = ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) )
24 13 14 16 orvclteel ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) ∈ dom 𝑃 )
25 21 23 15 24 fvmptd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ‘ 𝑛 ) = ( 𝑋 ∘RV/𝑐 ≤ 𝑛 ) )
26 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 = ( 𝑛 + 1 ) ) → 𝑖 = ( 𝑛 + 1 ) )
27 26 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 = ( 𝑛 + 1 ) ) → ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) = ( 𝑋 ∘RV/𝑐 ≤ ( 𝑛 + 1 ) ) )
28 13 14 18 orvclteel ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 ∘RV/𝑐 ≤ ( 𝑛 + 1 ) ) ∈ dom 𝑃 )
29 21 27 17 28 fvmptd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ‘ ( 𝑛 + 1 ) ) = ( 𝑋 ∘RV/𝑐 ≤ ( 𝑛 + 1 ) ) )
30 20 25 29 3sstr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ‘ 𝑛 ) ⊆ ( ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ‘ ( 𝑛 + 1 ) ) )
31 4 6 12 30 meascnbl ⊢ ( 𝜑 → ( 𝑃 ∘ ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) ( ⇝𝑡 ‘ ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) ) ( 𝑃 ‘ ∪ ran ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) )
32 measfn ⊢ ( 𝑃 ∈ ( measures ‘ dom 𝑃 ) → 𝑃 Fn dom 𝑃 )
33 dffn5 ⊢ ( 𝑃 Fn dom 𝑃 ↔ 𝑃 = ( 𝑎 ∈ dom 𝑃 ↦ ( 𝑃 ‘ 𝑎 ) ) )
34 33 biimpi ⊢ ( 𝑃 Fn dom 𝑃 → 𝑃 = ( 𝑎 ∈ dom 𝑃 ↦ ( 𝑃 ‘ 𝑎 ) ) )
35 6 32 34 3syl ⊢ ( 𝜑 → 𝑃 = ( 𝑎 ∈ dom 𝑃 ↦ ( 𝑃 ‘ 𝑎 ) ) )
36 prob01 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝑎 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝑎 ) ∈ ( 0 [,] 1 ) )
37 1 36 sylan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝑎 ) ∈ ( 0 [,] 1 ) )
38 35 37 fmpt3d ⊢ ( 𝜑 → 𝑃 : dom 𝑃 ⟶ ( 0 [,] 1 ) )
39 fco ⊢ ( ( 𝑃 : dom 𝑃 ⟶ ( 0 [,] 1 ) ∧ ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) : ℕ ⟶ dom 𝑃 ) → ( 𝑃 ∘ ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) : ℕ ⟶ ( 0 [,] 1 ) )
40 38 12 39 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∘ ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) : ℕ ⟶ ( 0 [,] 1 ) )
41 1 2 dstfrvunirn ⊢ ( 𝜑 → ∪ ran ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) = ∪ dom 𝑃 )
42 1 unveldomd ⊢ ( 𝜑 → ∪ dom 𝑃 ∈ dom 𝑃 )
43 41 42 eqeltrd ⊢ ( 𝜑 → ∪ ran ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ∈ dom 𝑃 )
44 prob01 ⊢ ( ( 𝑃 ∈ Prob ∧ ∪ ran ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ∈ dom 𝑃 ) → ( 𝑃 ‘ ∪ ran ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) ∈ ( 0 [,] 1 ) )
45 1 43 44 syl2anc ⊢ ( 𝜑 → ( 𝑃 ‘ ∪ ran ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) ∈ ( 0 [,] 1 ) )
46 0xr ⊢ 0 ∈ ℝ*
47 pnfxr ⊢ +∞ ∈ ℝ*
48 0le0 ⊢ 0 ≤ 0
49 1re ⊢ 1 ∈ ℝ
50 ltpnf ⊢ ( 1 ∈ ℝ → 1 < +∞ )
51 49 50 ax-mp ⊢ 1 < +∞
52 iccssico ⊢ ( ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 0 ≤ 0 ∧ 1 < +∞ ) ) → ( 0 [,] 1 ) ⊆ ( 0 [,) +∞ ) )
53 46 47 48 51 52 mp4an ⊢ ( 0 [,] 1 ) ⊆ ( 0 [,) +∞ )
54 4 40 45 53 lmlimxrge0 ⊢ ( 𝜑 → ( ( 𝑃 ∘ ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) ( ⇝𝑡 ‘ ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) ) ( 𝑃 ‘ ∪ ran ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) ↔ ( 𝑃 ∘ ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) ⇝ ( 𝑃 ‘ ∪ ran ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) ) )
55 31 54 mpbid ⊢ ( 𝜑 → ( 𝑃 ∘ ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) ⇝ ( 𝑃 ‘ ∪ ran ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) )
56 eqidd ⊢ ( 𝜑 → ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) = ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) )
57 fveq2 ⊢ ( 𝑎 = ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) → ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) )
58 11 56 35 57 fmptco ⊢ ( 𝜑 → ( 𝑃 ∘ ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) )
59 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 ≤ 𝑥 ) ) ) )
60 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑥 = 𝑖 ) → 𝑥 = 𝑖 )
61 60 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑥 = 𝑖 ) → ( 𝑋 ∘RV/𝑐 ≤ 𝑥 ) = ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) )
62 61 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑥 = 𝑖 ) → ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 ≤ 𝑥 ) ) = ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) )
63 7 11 probvalrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ∈ ℝ )
64 59 62 10 63 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) )
65 64 mpteq2dva ⊢ ( 𝜑 → ( 𝑖 ∈ ℕ ↦ ( 𝐹 ‘ 𝑖 ) ) = ( 𝑖 ∈ ℕ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) )
66 58 65 eqtr4d ⊢ ( 𝜑 → ( 𝑃 ∘ ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ ↦ ( 𝐹 ‘ 𝑖 ) ) )
67 41 fveq2d ⊢ ( 𝜑 → ( 𝑃 ‘ ∪ ran ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) = ( 𝑃 ‘ ∪ dom 𝑃 ) )
68 probtot ⊢ ( 𝑃 ∈ Prob → ( 𝑃 ‘ ∪ dom 𝑃 ) = 1 )
69 1 68 syl ⊢ ( 𝜑 → ( 𝑃 ‘ ∪ dom 𝑃 ) = 1 )
70 67 69 eqtrd ⊢ ( 𝜑 → ( 𝑃 ‘ ∪ ran ( 𝑖 ∈ ℕ ↦ ( 𝑋 ∘RV/𝑐 ≤ 𝑖 ) ) ) = 1 )
71 55 66 70 3brtr3d ⊢ ( 𝜑 → ( 𝑖 ∈ ℕ ↦ ( 𝐹 ‘ 𝑖 ) ) ⇝ 1 )
72 1z ⊢ 1 ∈ ℤ
73 reex ⊢ ℝ ∈ V
74 73 mptex ⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑃 ‘ ( 𝑋 ∘RV/𝑐 ≤ 𝑥 ) ) ) ∈ V
75 3 74 eqeltrdi ⊢ ( 𝜑 → 𝐹 ∈ V )
76 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
77 eqid ⊢ ( 𝑖 ∈ ℕ ↦ ( 𝐹 ‘ 𝑖 ) ) = ( 𝑖 ∈ ℕ ↦ ( 𝐹 ‘ 𝑖 ) )
78 76 77 climmpt ⊢ ( ( 1 ∈ ℤ ∧ 𝐹 ∈ V ) → ( 𝐹 ⇝ 1 ↔ ( 𝑖 ∈ ℕ ↦ ( 𝐹 ‘ 𝑖 ) ) ⇝ 1 ) )
79 72 75 78 sylancr ⊢ ( 𝜑 → ( 𝐹 ⇝ 1 ↔ ( 𝑖 ∈ ℕ ↦ ( 𝐹 ‘ 𝑖 ) ) ⇝ 1 ) )
80 71 79 mpbird ⊢ ( 𝜑 → 𝐹 ⇝ 1 )