Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))) =
(TopOpen‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
2 | | dstfrv.1 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ Prob) |
3 | | domprobmeas 29799 |
. . . . . 6
⊢ (𝑃 ∈ Prob → 𝑃 ∈ (measures‘dom
𝑃)) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ (measures‘dom 𝑃)) |
5 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑃 ∈ Prob) |
6 | | dstfrv.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) |
7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑋 ∈ (rRndVar‘𝑃)) |
8 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ) |
9 | 8 | nnred 10912 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℝ) |
10 | 5, 7, 9 | orvclteel 29861 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑖) ∈ dom 𝑃) |
11 | | eqid 2610 |
. . . . . 6
⊢ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐
≤ 𝑖)) = (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐
≤ 𝑖)) |
12 | 10, 11 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)):ℕ⟶dom 𝑃) |
13 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ Prob) |
14 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ (rRndVar‘𝑃)) |
15 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
16 | 15 | nnred 10912 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ) |
17 | 15 | peano2nnd 10914 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
18 | 17 | nnred 10912 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ) |
19 | 16 | lep1d 10834 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≤ (𝑛 + 1)) |
20 | 13, 14, 16, 18, 19 | orvclteinc 29864 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑛) ⊆ (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
21 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) |
22 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = 𝑛) → 𝑖 = 𝑛) |
23 | 22 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = 𝑛) → (𝑋∘RV/𝑐 ≤ 𝑖) = (𝑋∘RV/𝑐 ≤ 𝑛)) |
24 | 13, 14, 16 | orvclteel 29861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑛) ∈ dom 𝑃) |
25 | 21, 23, 15, 24 | fvmptd 6197 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘𝑛) = (𝑋∘RV/𝑐 ≤ 𝑛)) |
26 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = (𝑛 + 1)) → 𝑖 = (𝑛 + 1)) |
27 | 26 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = (𝑛 + 1)) → (𝑋∘RV/𝑐 ≤ 𝑖) = (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
28 | 13, 14, 18 | orvclteel 29861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ (𝑛 + 1)) ∈ dom 𝑃) |
29 | 21, 27, 17, 28 | fvmptd 6197 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘(𝑛 + 1)) = (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
30 | 20, 25, 29 | 3sstr4d 3611 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘𝑛) ⊆ ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘(𝑛 + 1))) |
31 | 1, 4, 12, 30 | meascnbl 29609 |
. . . 4
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))(⇝𝑡‘(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))))(𝑃‘∪
ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))) |
32 | | measfn 29594 |
. . . . . . . 8
⊢ (𝑃 ∈ (measures‘dom
𝑃) → 𝑃 Fn dom 𝑃) |
33 | | dffn5 6151 |
. . . . . . . . 9
⊢ (𝑃 Fn dom 𝑃 ↔ 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
34 | 33 | biimpi 205 |
. . . . . . . 8
⊢ (𝑃 Fn dom 𝑃 → 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
35 | 4, 32, 34 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
36 | | prob01 29802 |
. . . . . . . 8
⊢ ((𝑃 ∈ Prob ∧ 𝑎 ∈ dom 𝑃) → (𝑃‘𝑎) ∈ (0[,]1)) |
37 | 2, 36 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑃) → (𝑃‘𝑎) ∈ (0[,]1)) |
38 | 35, 37 | fmpt3d 6293 |
. . . . . 6
⊢ (𝜑 → 𝑃:dom 𝑃⟶(0[,]1)) |
39 | | fco 5971 |
. . . . . 6
⊢ ((𝑃:dom 𝑃⟶(0[,]1) ∧ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)):ℕ⟶dom 𝑃) → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))):ℕ⟶(0[,]1)) |
40 | 38, 12, 39 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))):ℕ⟶(0[,]1)) |
41 | 2, 6 | dstfrvunirn 29863 |
. . . . . . 7
⊢ (𝜑 → ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = ∪ dom 𝑃) |
42 | 2 | unveldomd 29804 |
. . . . . . 7
⊢ (𝜑 → ∪ dom 𝑃 ∈ dom 𝑃) |
43 | 41, 42 | eqeltrd 2688 |
. . . . . 6
⊢ (𝜑 → ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) ∈ dom 𝑃) |
44 | | prob01 29802 |
. . . . . 6
⊢ ((𝑃 ∈ Prob ∧ ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) ∈ dom 𝑃) → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) ∈
(0[,]1)) |
45 | 2, 43, 44 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) ∈
(0[,]1)) |
46 | | 0xr 9965 |
. . . . . 6
⊢ 0 ∈
ℝ* |
47 | | pnfxr 9971 |
. . . . . 6
⊢ +∞
∈ ℝ* |
48 | | 0le0 10987 |
. . . . . 6
⊢ 0 ≤
0 |
49 | | 1re 9918 |
. . . . . . 7
⊢ 1 ∈
ℝ |
50 | | ltpnf 11830 |
. . . . . . 7
⊢ (1 ∈
ℝ → 1 < +∞) |
51 | 49, 50 | ax-mp 5 |
. . . . . 6
⊢ 1 <
+∞ |
52 | | iccssico 12116 |
. . . . . 6
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
≤ 0 ∧ 1 < +∞)) → (0[,]1) ⊆
(0[,)+∞)) |
53 | 46, 47, 48, 51, 52 | mp4an 705 |
. . . . 5
⊢ (0[,]1)
⊆ (0[,)+∞) |
54 | 1, 40, 45, 53 | lmlimxrge0 29322 |
. . . 4
⊢ (𝜑 → ((𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))(⇝𝑡‘(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))))(𝑃‘∪
ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))
↔ (𝑃 ∘ (𝑖
∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) ⇝ (𝑃‘∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))))) |
55 | 31, 54 | mpbid 221 |
. . 3
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) ⇝ (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖)))) |
56 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) |
57 | | fveq2 6103 |
. . . . 5
⊢ (𝑎 = (𝑋∘RV/𝑐 ≤ 𝑖) → (𝑃‘𝑎) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
58 | 10, 56, 35, 57 | fmptco 6303 |
. . . 4
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑖 ∈ ℕ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)))) |
59 | | dstfrv.3 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) |
60 | 59 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) |
61 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → 𝑥 = 𝑖) |
62 | 61 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → (𝑋∘RV/𝑐 ≤ 𝑥) = (𝑋∘RV/𝑐 ≤ 𝑖)) |
63 | 62 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
64 | 5, 10 | probvalrnd 29813 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)) ∈
ℝ) |
65 | 60, 63, 9, 64 | fvmptd 6197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
66 | 65 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) = (𝑖 ∈ ℕ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)))) |
67 | 58, 66 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑖 ∈ ℕ ↦ (𝐹‘𝑖))) |
68 | 41 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑃‘∪ dom
𝑃)) |
69 | | probtot 29801 |
. . . . 5
⊢ (𝑃 ∈ Prob → (𝑃‘∪ dom 𝑃) = 1) |
70 | 2, 69 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑃‘∪ dom
𝑃) = 1) |
71 | 68, 70 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) = 1) |
72 | 55, 67, 71 | 3brtr3d 4614 |
. 2
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) ⇝ 1) |
73 | | 1z 11284 |
. . 3
⊢ 1 ∈
ℤ |
74 | | reex 9906 |
. . . . 5
⊢ ℝ
∈ V |
75 | 74 | mptex 6390 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥))) ∈ V |
76 | 59, 75 | syl6eqel 2696 |
. . 3
⊢ (𝜑 → 𝐹 ∈ V) |
77 | | nnuz 11599 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
78 | | eqid 2610 |
. . . 4
⊢ (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) = (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) |
79 | 77, 78 | climmpt 14150 |
. . 3
⊢ ((1
∈ ℤ ∧ 𝐹
∈ V) → (𝐹 ⇝
1 ↔ (𝑖 ∈ ℕ
↦ (𝐹‘𝑖)) ⇝ 1)) |
80 | 73, 76, 79 | sylancr 694 |
. 2
⊢ (𝜑 → (𝐹 ⇝ 1 ↔ (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) ⇝ 1)) |
81 | 72, 80 | mpbird 246 |
1
⊢ (𝜑 → 𝐹 ⇝ 1) |