| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))) =
(TopOpen‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
| 2 | | dstfrv.1 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ Prob) |
| 3 | | domprobmeas 34412 |
. . . . . 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 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ) |
| 9 | 8 | nnred 12281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℝ) |
| 10 | 5, 7, 9 | orvclteel 34475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑖) ∈ dom 𝑃) |
| 11 | 10 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)):ℕ⟶dom 𝑃) |
| 12 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ Prob) |
| 13 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ (rRndVar‘𝑃)) |
| 14 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
| 15 | 14 | nnred 12281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ) |
| 16 | 14 | peano2nnd 12283 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
| 17 | 16 | nnred 12281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ) |
| 18 | 15 | lep1d 12199 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≤ (𝑛 + 1)) |
| 19 | 12, 13, 15, 17, 18 | orvclteinc 34478 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑛) ⊆ (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
| 20 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) |
| 21 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = 𝑛) → 𝑖 = 𝑛) |
| 22 | 21 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = 𝑛) → (𝑋∘RV/𝑐 ≤ 𝑖) = (𝑋∘RV/𝑐 ≤ 𝑛)) |
| 23 | 12, 13, 15 | orvclteel 34475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ 𝑛) ∈ dom 𝑃) |
| 24 | 20, 22, 14, 23 | fvmptd 7023 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘𝑛) = (𝑋∘RV/𝑐 ≤ 𝑛)) |
| 25 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = (𝑛 + 1)) → 𝑖 = (𝑛 + 1)) |
| 26 | 25 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑖 = (𝑛 + 1)) → (𝑋∘RV/𝑐 ≤ 𝑖) = (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
| 27 | 12, 13, 17 | orvclteel 34475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋∘RV/𝑐 ≤ (𝑛 + 1)) ∈ dom 𝑃) |
| 28 | 20, 26, 16, 27 | fvmptd 7023 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘(𝑛 + 1)) = (𝑋∘RV/𝑐 ≤ (𝑛 + 1))) |
| 29 | 19, 24, 28 | 3sstr4d 4039 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘𝑛) ⊆ ((𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))‘(𝑛 + 1))) |
| 30 | 1, 4, 11, 29 | meascnbl 34220 |
. . . 4
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))(⇝𝑡‘(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))))(𝑃‘∪
ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))) |
| 31 | | measfn 34205 |
. . . . . . . 8
⊢ (𝑃 ∈ (measures‘dom
𝑃) → 𝑃 Fn dom 𝑃) |
| 32 | | dffn5 6967 |
. . . . . . . . 9
⊢ (𝑃 Fn dom 𝑃 ↔ 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
| 33 | 32 | biimpi 216 |
. . . . . . . 8
⊢ (𝑃 Fn dom 𝑃 → 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
| 34 | 4, 31, 33 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑃 = (𝑎 ∈ dom 𝑃 ↦ (𝑃‘𝑎))) |
| 35 | | prob01 34415 |
. . . . . . . 8
⊢ ((𝑃 ∈ Prob ∧ 𝑎 ∈ dom 𝑃) → (𝑃‘𝑎) ∈ (0[,]1)) |
| 36 | 2, 35 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑃) → (𝑃‘𝑎) ∈ (0[,]1)) |
| 37 | 34, 36 | fmpt3d 7136 |
. . . . . 6
⊢ (𝜑 → 𝑃:dom 𝑃⟶(0[,]1)) |
| 38 | | fco 6760 |
. . . . . 6
⊢ ((𝑃:dom 𝑃⟶(0[,]1) ∧ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)):ℕ⟶dom 𝑃) → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))):ℕ⟶(0[,]1)) |
| 39 | 37, 11, 38 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))):ℕ⟶(0[,]1)) |
| 40 | 2, 6 | dstfrvunirn 34477 |
. . . . . . 7
⊢ (𝜑 → ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = ∪ dom 𝑃) |
| 41 | 2 | unveldomd 34417 |
. . . . . . 7
⊢ (𝜑 → ∪ dom 𝑃 ∈ dom 𝑃) |
| 42 | 40, 41 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) ∈ dom 𝑃) |
| 43 | | prob01 34415 |
. . . . . 6
⊢ ((𝑃 ∈ Prob ∧ ∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) ∈ dom 𝑃) → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) ∈
(0[,]1)) |
| 44 | 2, 42, 43 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) ∈
(0[,]1)) |
| 45 | | 0xr 11308 |
. . . . . 6
⊢ 0 ∈
ℝ* |
| 46 | | pnfxr 11315 |
. . . . . 6
⊢ +∞
∈ ℝ* |
| 47 | | 0le0 12367 |
. . . . . 6
⊢ 0 ≤
0 |
| 48 | | 1re 11261 |
. . . . . . 7
⊢ 1 ∈
ℝ |
| 49 | | ltpnf 13162 |
. . . . . . 7
⊢ (1 ∈
ℝ → 1 < +∞) |
| 50 | 48, 49 | ax-mp 5 |
. . . . . 6
⊢ 1 <
+∞ |
| 51 | | iccssico 13459 |
. . . . . 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 33947 |
. . . 4
⊢ (𝜑 → ((𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))(⇝𝑡‘(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))))(𝑃‘∪
ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)))
↔ (𝑃 ∘ (𝑖
∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) ⇝ (𝑃‘∪ ran (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))))) |
| 54 | 30, 53 | mpbid 232 |
. . 3
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) ⇝ (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖)))) |
| 55 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖)) = (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) |
| 56 | | fveq2 6906 |
. . . . 5
⊢ (𝑎 = (𝑋∘RV/𝑐 ≤ 𝑖) → (𝑃‘𝑎) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
| 57 | 10, 55, 34, 56 | fmptco 7149 |
. . . 4
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑖 ∈ ℕ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)))) |
| 58 | | dstfrv.3 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) |
| 59 | 58 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) |
| 60 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → 𝑥 = 𝑖) |
| 61 | 60 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → (𝑋∘RV/𝑐 ≤ 𝑥) = (𝑋∘RV/𝑐 ≤ 𝑖)) |
| 62 | 61 | fveq2d 6910 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ 𝑥 = 𝑖) → (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
| 63 | 5, 10 | probvalrnd 34426 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)) ∈
ℝ) |
| 64 | 59, 62, 9, 63 | fvmptd 7023 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) = (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖))) |
| 65 | 64 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) = (𝑖 ∈ ℕ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑖)))) |
| 66 | 57, 65 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → (𝑃 ∘ (𝑖 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑖 ∈ ℕ ↦ (𝐹‘𝑖))) |
| 67 | 40 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) = (𝑃‘∪ dom
𝑃)) |
| 68 | | probtot 34414 |
. . . . 5
⊢ (𝑃 ∈ Prob → (𝑃‘∪ dom 𝑃) = 1) |
| 69 | 2, 68 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑃‘∪ dom
𝑃) = 1) |
| 70 | 67, 69 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (𝑃‘∪ ran
(𝑖 ∈ ℕ ↦
(𝑋∘RV/𝑐 ≤ 𝑖))) = 1) |
| 71 | 54, 66, 70 | 3brtr3d 5174 |
. 2
⊢ (𝜑 → (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) ⇝ 1) |
| 72 | | 1z 12647 |
. . 3
⊢ 1 ∈
ℤ |
| 73 | | reex 11246 |
. . . . 5
⊢ ℝ
∈ V |
| 74 | 73 | mptex 7243 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥))) ∈ V |
| 75 | 58, 74 | eqeltrdi 2849 |
. . 3
⊢ (𝜑 → 𝐹 ∈ V) |
| 76 | | nnuz 12921 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
| 77 | | eqid 2737 |
. . . 4
⊢ (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) = (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) |
| 78 | 76, 77 | climmpt 15607 |
. . 3
⊢ ((1
∈ ℤ ∧ 𝐹
∈ V) → (𝐹 ⇝
1 ↔ (𝑖 ∈ ℕ
↦ (𝐹‘𝑖)) ⇝ 1)) |
| 79 | 72, 75, 78 | sylancr 587 |
. 2
⊢ (𝜑 → (𝐹 ⇝ 1 ↔ (𝑖 ∈ ℕ ↦ (𝐹‘𝑖)) ⇝ 1)) |
| 80 | 71, 79 | mpbird 257 |
1
⊢ (𝜑 → 𝐹 ⇝ 1) |