Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . 5
⊢
(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))) =
(TopOpen‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
2 | | dstfrv.1 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ Prob) |
3 | | domprobmeas 32377 |
. . . . . 6
⊢ (𝑃 ∈ Prob → 𝑃 ∈ (measures‘dom
𝑃)) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ (measures‘dom 𝑃)) |
5 | 2 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑃 ∈ Prob) |
6 | | dstfrv.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) |
7 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑋 ∈ (rRndVar‘𝑃)) |
8 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ) |
9 | 8 | nnred 11988 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℝ) |
10 | 5, 7, 9 | orvclteel 32439 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑖) ∈ dom 𝑃) |
11 | 10 | fmpttd 6989 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)):ℕ⟶dom 𝑃) |
12 | 2 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ Prob) |
13 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ (rRndVar‘𝑃)) |
14 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
15 | 14 | nnred 11988 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ) |
16 | 14 | peano2nnd 11990 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
17 | 16 | nnred 11988 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ) |
18 | 15 | lep1d 11906 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≤ (𝑛 + 1)) |
19 | 12, 13, 15, 17, 18 | orvclteinc 32442 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑛) ⊆ (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
20 | | eqidd 2739 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) |
21 | | simpr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = 𝑛) → 𝑖 = 𝑛) |
22 | 21 | oveq2d 7291 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = 𝑛) → (𝑋∘RV/𝑐 ≤ 𝑖) = (𝑋∘RV/𝑐 ≤ 𝑛)) |
23 | 12, 13, 15 | orvclteel 32439 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑛) ∈ dom 𝑃) |
24 | 20, 22, 14, 23 | fvmptd 6882 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘𝑛) = (𝑋∘RV/𝑐 ≤ 𝑛)) |
25 | | simpr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = (𝑛 + 1)) → 𝑖 = (𝑛 + 1)) |
26 | 25 | oveq2d 7291 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = (𝑛 + 1)) → (𝑋∘RV/𝑐 ≤ 𝑖) = (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
27 | 12, 13, 17 | orvclteel 32439 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ (𝑛 + 1)) ∈ dom 𝑃) |
28 | 20, 26, 16, 27 | fvmptd 6882 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘(𝑛 + 1)) = (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
29 | 19, 24, 28 | 3sstr4d 3968 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘𝑛) ⊆ ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘(𝑛 + 1))) |
30 | 1, 4, 11, 29 | meascnbl 32187 |
. . . 4
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))(⇝𝑡‘(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))))(𝑃‘∪
ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))) |
31 | | measfn 32172 |
. . . . . . . 8
⊢ (𝑃 ∈ (measures‘dom
𝑃) → 𝑃 Fn dom 𝑃) |
32 | | dffn5 6828 |
. . . . . . . . 9
⊢ (𝑃 Fn dom 𝑃 ↔ 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
33 | 32 | biimpi 215 |
. . . . . . . 8
⊢ (𝑃 Fn dom 𝑃 → 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
34 | 4, 31, 33 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
35 | | prob01 32380 |
. . . . . . . 8
⊢ ((𝑃 ∈ Prob ∧ 𝑎 ∈ dom 𝑃) → (𝑃‘𝑎) ∈ (0[,]1)) |
36 | 2, 35 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑃) → (𝑃‘𝑎) ∈ (0[,]1)) |
37 | 34, 36 | fmpt3d 6990 |
. . . . . 6
⊢ (𝜑 → 𝑃:dom 𝑃⟶(0[,]1)) |
38 | | fco 6624 |
. . . . . 6
⊢ ((𝑃:dom 𝑃⟶(0[,]1) ∧ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)):ℕ⟶dom 𝑃) → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))):ℕ⟶(0[,]1)) |
39 | 37, 11, 38 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))):ℕ⟶(0[,]1)) |
40 | 2, 6 | dstfrvunirn 32441 |
. . . . . . 7
⊢ (𝜑 → ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = ∪ dom 𝑃) |
41 | 2 | unveldomd 32382 |
. . . . . . 7
⊢ (𝜑 → ∪ dom 𝑃 ∈ dom 𝑃) |
42 | 40, 41 | eqeltrd 2839 |
. . . . . 6
⊢ (𝜑 → ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) ∈ dom 𝑃) |
43 | | prob01 32380 |
. . . . . 6
⊢ ((𝑃 ∈ Prob ∧ ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) ∈ dom 𝑃) → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) ∈
(0[,]1)) |
44 | 2, 42, 43 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) ∈
(0[,]1)) |
45 | | 0xr 11022 |
. . . . . 6
⊢ 0 ∈
ℝ* |
46 | | pnfxr 11029 |
. . . . . 6
⊢ +∞
∈ ℝ* |
47 | | 0le0 12074 |
. . . . . 6
⊢ 0 ≤
0 |
48 | | 1re 10975 |
. . . . . . 7
⊢ 1 ∈
ℝ |
49 | | ltpnf 12856 |
. . . . . . 7
⊢ (1 ∈
ℝ → 1 < +∞) |
50 | 48, 49 | ax-mp 5 |
. . . . . 6
⊢ 1 <
+∞ |
51 | | iccssico 13151 |
. . . . . 6
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
≤ 0 ∧ 1 < +∞)) → (0[,]1) ⊆
(0[,)+∞)) |
52 | 45, 46, 47, 50, 51 | mp4an 690 |
. . . . 5
⊢ (0[,]1)
⊆ (0[,)+∞) |
53 | 1, 39, 44, 52 | lmlimxrge0 31898 |
. . . 4
⊢ (𝜑 → ((𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))(⇝𝑡‘(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))))(𝑃‘∪
ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))
↔ (𝑃 ∘ (𝑖
∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) ⇝ (𝑃‘∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))))) |
54 | 30, 53 | mpbid 231 |
. . 3
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) ⇝ (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖)))) |
55 | | eqidd 2739 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) |
56 | | fveq2 6774 |
. . . . 5
⊢ (𝑎 = (𝑋∘RV/𝑐 ≤ 𝑖) → (𝑃‘𝑎) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
57 | 10, 55, 34, 56 | fmptco 7001 |
. . . 4
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑖 ∈ ℕ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)))) |
58 | | dstfrv.3 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) |
59 | 58 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) |
60 | | simpr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → 𝑥 = 𝑖) |
61 | 60 | oveq2d 7291 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → (𝑋∘RV/𝑐 ≤ 𝑥) = (𝑋∘RV/𝑐 ≤ 𝑖)) |
62 | 61 | fveq2d 6778 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
63 | 5, 10 | probvalrnd 32391 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)) ∈
ℝ) |
64 | 59, 62, 9, 63 | fvmptd 6882 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
65 | 64 | mpteq2dva 5174 |
. . . 4
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) = (𝑖 ∈ ℕ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)))) |
66 | 57, 65 | eqtr4d 2781 |
. . 3
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑖 ∈ ℕ ↦ (𝐹‘𝑖))) |
67 | 40 | fveq2d 6778 |
. . . 4
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑃‘∪ dom
𝑃)) |
68 | | probtot 32379 |
. . . . 5
⊢ (𝑃 ∈ Prob → (𝑃‘∪ dom 𝑃) = 1) |
69 | 2, 68 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑃‘∪ dom
𝑃) = 1) |
70 | 67, 69 | eqtrd 2778 |
. . 3
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) = 1) |
71 | 54, 66, 70 | 3brtr3d 5105 |
. 2
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) ⇝ 1) |
72 | | 1z 12350 |
. . 3
⊢ 1 ∈
ℤ |
73 | | reex 10962 |
. . . . 5
⊢ ℝ
∈ V |
74 | 73 | mptex 7099 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥))) ∈ V |
75 | 58, 74 | eqeltrdi 2847 |
. . 3
⊢ (𝜑 → 𝐹 ∈ V) |
76 | | nnuz 12621 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
77 | | eqid 2738 |
. . . 4
⊢ (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) = (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) |
78 | 76, 77 | climmpt 15280 |
. . 3
⊢ ((1
∈ ℤ ∧ 𝐹
∈ V) → (𝐹 ⇝
1 ↔ (𝑖 ∈ ℕ
↦ (𝐹‘𝑖)) ⇝ 1)) |
79 | 72, 75, 78 | sylancr 587 |
. 2
⊢ (𝜑 → (𝐹 ⇝ 1 ↔ (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) ⇝ 1)) |
80 | 71, 79 | mpbird 256 |
1
⊢ (𝜑 → 𝐹 ⇝ 1) |