Step | Hyp | Ref
| Expression |
1 | | eqid 2739 |
. . . . 5
⊢
(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))) =
(TopOpen‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
2 | | dstfrv.1 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ Prob) |
3 | | domprobmeas 31960 |
. . . . . 6
⊢ (𝑃 ∈ Prob → 𝑃 ∈ (measures‘dom
𝑃)) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ (measures‘dom 𝑃)) |
5 | 2 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑃 ∈ Prob) |
6 | | dstfrv.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) |
7 | 6 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑋 ∈ (rRndVar‘𝑃)) |
8 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ) |
9 | 8 | nnred 11744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℝ) |
10 | 5, 7, 9 | orvclteel 32022 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑖) ∈ dom 𝑃) |
11 | 10 | fmpttd 6902 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)):ℕ⟶dom 𝑃) |
12 | 2 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ Prob) |
13 | 6 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ (rRndVar‘𝑃)) |
14 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
15 | 14 | nnred 11744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ) |
16 | 14 | peano2nnd 11746 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
17 | 16 | nnred 11744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ) |
18 | 15 | lep1d 11662 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≤ (𝑛 + 1)) |
19 | 12, 13, 15, 17, 18 | orvclteinc 32025 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑛) ⊆ (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
20 | | eqidd 2740 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) |
21 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = 𝑛) → 𝑖 = 𝑛) |
22 | 21 | oveq2d 7199 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = 𝑛) → (𝑋∘RV/𝑐 ≤ 𝑖) = (𝑋∘RV/𝑐 ≤ 𝑛)) |
23 | 12, 13, 15 | orvclteel 32022 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑛) ∈ dom 𝑃) |
24 | 20, 22, 14, 23 | fvmptd 6795 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘𝑛) = (𝑋∘RV/𝑐 ≤ 𝑛)) |
25 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = (𝑛 + 1)) → 𝑖 = (𝑛 + 1)) |
26 | 25 | oveq2d 7199 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = (𝑛 + 1)) → (𝑋∘RV/𝑐 ≤ 𝑖) = (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
27 | 12, 13, 17 | orvclteel 32022 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ (𝑛 + 1)) ∈ dom 𝑃) |
28 | 20, 26, 16, 27 | fvmptd 6795 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘(𝑛 + 1)) = (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
29 | 19, 24, 28 | 3sstr4d 3934 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘𝑛) ⊆ ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘(𝑛 + 1))) |
30 | 1, 4, 11, 29 | meascnbl 31770 |
. . . 4
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))(⇝𝑡‘(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))))(𝑃‘∪
ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))) |
31 | | measfn 31755 |
. . . . . . . 8
⊢ (𝑃 ∈ (measures‘dom
𝑃) → 𝑃 Fn dom 𝑃) |
32 | | dffn5 6741 |
. . . . . . . . 9
⊢ (𝑃 Fn dom 𝑃 ↔ 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
33 | 32 | biimpi 219 |
. . . . . . . 8
⊢ (𝑃 Fn dom 𝑃 → 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
34 | 4, 31, 33 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
35 | | prob01 31963 |
. . . . . . . 8
⊢ ((𝑃 ∈ Prob ∧ 𝑎 ∈ dom 𝑃) → (𝑃‘𝑎) ∈ (0[,]1)) |
36 | 2, 35 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑃) → (𝑃‘𝑎) ∈ (0[,]1)) |
37 | 34, 36 | fmpt3d 6903 |
. . . . . 6
⊢ (𝜑 → 𝑃:dom 𝑃⟶(0[,]1)) |
38 | | fco 6539 |
. . . . . 6
⊢ ((𝑃:dom 𝑃⟶(0[,]1) ∧ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)):ℕ⟶dom 𝑃) → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))):ℕ⟶(0[,]1)) |
39 | 37, 11, 38 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))):ℕ⟶(0[,]1)) |
40 | 2, 6 | dstfrvunirn 32024 |
. . . . . . 7
⊢ (𝜑 → ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = ∪ dom 𝑃) |
41 | 2 | unveldomd 31965 |
. . . . . . 7
⊢ (𝜑 → ∪ dom 𝑃 ∈ dom 𝑃) |
42 | 40, 41 | eqeltrd 2834 |
. . . . . 6
⊢ (𝜑 → ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) ∈ dom 𝑃) |
43 | | prob01 31963 |
. . . . . 6
⊢ ((𝑃 ∈ Prob ∧ ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) ∈ dom 𝑃) → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) ∈
(0[,]1)) |
44 | 2, 42, 43 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) ∈
(0[,]1)) |
45 | | 0xr 10779 |
. . . . . 6
⊢ 0 ∈
ℝ* |
46 | | pnfxr 10786 |
. . . . . 6
⊢ +∞
∈ ℝ* |
47 | | 0le0 11830 |
. . . . . 6
⊢ 0 ≤
0 |
48 | | 1re 10732 |
. . . . . . 7
⊢ 1 ∈
ℝ |
49 | | ltpnf 12611 |
. . . . . . 7
⊢ (1 ∈
ℝ → 1 < +∞) |
50 | 48, 49 | ax-mp 5 |
. . . . . 6
⊢ 1 <
+∞ |
51 | | iccssico 12906 |
. . . . . 6
⊢ (((0
∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (0
≤ 0 ∧ 1 < +∞)) → (0[,]1) ⊆
(0[,)+∞)) |
52 | 45, 46, 47, 50, 51 | mp4an 693 |
. . . . 5
⊢ (0[,]1)
⊆ (0[,)+∞) |
53 | 1, 39, 44, 52 | lmlimxrge0 31483 |
. . . 4
⊢ (𝜑 → ((𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))(⇝𝑡‘(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))))(𝑃‘∪
ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))
↔ (𝑃 ∘ (𝑖
∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) ⇝ (𝑃‘∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))))) |
54 | 30, 53 | mpbid 235 |
. . 3
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) ⇝ (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖)))) |
55 | | eqidd 2740 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) |
56 | | fveq2 6687 |
. . . . 5
⊢ (𝑎 = (𝑋∘RV/𝑐 ≤ 𝑖) → (𝑃‘𝑎) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
57 | 10, 55, 34, 56 | fmptco 6914 |
. . . 4
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑖 ∈ ℕ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)))) |
58 | | dstfrv.3 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) |
59 | 58 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) |
60 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → 𝑥 = 𝑖) |
61 | 60 | oveq2d 7199 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → (𝑋∘RV/𝑐 ≤ 𝑥) = (𝑋∘RV/𝑐 ≤ 𝑖)) |
62 | 61 | fveq2d 6691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
63 | 5, 10 | probvalrnd 31974 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)) ∈
ℝ) |
64 | 59, 62, 9, 63 | fvmptd 6795 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
65 | 64 | mpteq2dva 5135 |
. . . 4
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) = (𝑖 ∈ ℕ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)))) |
66 | 57, 65 | eqtr4d 2777 |
. . 3
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑖 ∈ ℕ ↦ (𝐹‘𝑖))) |
67 | 40 | fveq2d 6691 |
. . . 4
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑃‘∪ dom
𝑃)) |
68 | | probtot 31962 |
. . . . 5
⊢ (𝑃 ∈ Prob → (𝑃‘∪ dom 𝑃) = 1) |
69 | 2, 68 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑃‘∪ dom
𝑃) = 1) |
70 | 67, 69 | eqtrd 2774 |
. . 3
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) = 1) |
71 | 54, 66, 70 | 3brtr3d 5071 |
. 2
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) ⇝ 1) |
72 | | 1z 12106 |
. . 3
⊢ 1 ∈
ℤ |
73 | | reex 10719 |
. . . . 5
⊢ ℝ
∈ V |
74 | 73 | mptex 7009 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥))) ∈ V |
75 | 58, 74 | eqeltrdi 2842 |
. . 3
⊢ (𝜑 → 𝐹 ∈ V) |
76 | | nnuz 12376 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
77 | | eqid 2739 |
. . . 4
⊢ (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) = (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) |
78 | 76, 77 | climmpt 15031 |
. . 3
⊢ ((1
∈ ℤ ∧ 𝐹
∈ V) → (𝐹 ⇝
1 ↔ (𝑖 ∈ ℕ
↦ (𝐹‘𝑖)) ⇝ 1)) |
79 | 72, 75, 78 | sylancr 590 |
. 2
⊢ (𝜑 → (𝐹 ⇝ 1 ↔ (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) ⇝ 1)) |
80 | 71, 79 | mpbird 260 |
1
⊢ (𝜑 → 𝐹 ⇝ 1) |