| Step | Hyp | Ref
| Expression |
| 1 | | 0re 11263 |
. . . . 5
⊢ 0 ∈
ℝ |
| 2 | 1 | rgenw 3065 |
. . . 4
⊢
∀𝑥 ∈
∪ dom 𝑃0 ∈ ℝ |
| 3 | | eqid 2737 |
. . . . 5
⊢ (𝑥 ∈ ∪ dom 𝑃 ↦ 0) = (𝑥 ∈ ∪ dom
𝑃 ↦
0) |
| 4 | 3 | fmpt 7130 |
. . . 4
⊢
(∀𝑥 ∈
∪ dom 𝑃0 ∈ ℝ ↔ (𝑥 ∈ ∪ dom
𝑃 ↦ 0):∪ dom 𝑃⟶ℝ) |
| 5 | 2, 4 | mpbi 230 |
. . 3
⊢ (𝑥 ∈ ∪ dom 𝑃 ↦ 0):∪ dom
𝑃⟶ℝ |
| 6 | 5 | a1i 11 |
. 2
⊢ (𝜑 → (𝑥 ∈ ∪ dom
𝑃 ↦ 0):∪ dom 𝑃⟶ℝ) |
| 7 | | fconstmpt 5747 |
. . . . . . . . . 10
⊢ (∪ dom 𝑃 × {0}) = (𝑥 ∈ ∪ dom
𝑃 ↦
0) |
| 8 | 7 | cnveqi 5885 |
. . . . . . . . 9
⊢ ◡(∪ dom 𝑃 × {0}) = ◡(𝑥 ∈ ∪ dom
𝑃 ↦
0) |
| 9 | | cnvxp 6177 |
. . . . . . . . 9
⊢ ◡(∪ dom 𝑃 × {0}) = ({0} ×
∪ dom 𝑃) |
| 10 | 8, 9 | eqtr3i 2767 |
. . . . . . . 8
⊢ ◡(𝑥 ∈ ∪ dom
𝑃 ↦ 0) = ({0} ×
∪ dom 𝑃) |
| 11 | 10 | imaeq1i 6075 |
. . . . . . 7
⊢ (◡(𝑥 ∈ ∪ dom
𝑃 ↦ 0) “ 𝑦) = (({0} × ∪ dom 𝑃) “ 𝑦) |
| 12 | | df-ima 5698 |
. . . . . . 7
⊢ (({0}
× ∪ dom 𝑃) “ 𝑦) = ran (({0} × ∪ dom 𝑃) ↾ 𝑦) |
| 13 | | df-rn 5696 |
. . . . . . 7
⊢ ran (({0}
× ∪ dom 𝑃) ↾ 𝑦) = dom ◡(({0} × ∪
dom 𝑃) ↾ 𝑦) |
| 14 | 11, 12, 13 | 3eqtri 2769 |
. . . . . 6
⊢ (◡(𝑥 ∈ ∪ dom
𝑃 ↦ 0) “ 𝑦) = dom ◡(({0} × ∪
dom 𝑃) ↾ 𝑦) |
| 15 | | df-res 5697 |
. . . . . . . . 9
⊢ (({0}
× ∪ dom 𝑃) ↾ 𝑦) = (({0} × ∪ dom 𝑃) ∩ (𝑦 × V)) |
| 16 | | inxp 5842 |
. . . . . . . . 9
⊢ (({0}
× ∪ dom 𝑃) ∩ (𝑦 × V)) = (({0} ∩ 𝑦) × (∪ dom
𝑃 ∩
V)) |
| 17 | | inv1 4398 |
. . . . . . . . . 10
⊢ (∪ dom 𝑃 ∩ V) = ∪ dom
𝑃 |
| 18 | 17 | xpeq2i 5712 |
. . . . . . . . 9
⊢ (({0}
∩ 𝑦) × (∪ dom 𝑃 ∩ V)) = (({0} ∩ 𝑦) × ∪ dom
𝑃) |
| 19 | 15, 16, 18 | 3eqtri 2769 |
. . . . . . . 8
⊢ (({0}
× ∪ dom 𝑃) ↾ 𝑦) = (({0} ∩ 𝑦) × ∪ dom
𝑃) |
| 20 | 19 | cnveqi 5885 |
. . . . . . 7
⊢ ◡(({0} × ∪
dom 𝑃) ↾ 𝑦) = ◡(({0} ∩ 𝑦) × ∪ dom
𝑃) |
| 21 | 20 | dmeqi 5915 |
. . . . . 6
⊢ dom ◡(({0} × ∪
dom 𝑃) ↾ 𝑦) = dom ◡(({0} ∩ 𝑦) × ∪ dom
𝑃) |
| 22 | | cnvxp 6177 |
. . . . . . 7
⊢ ◡(({0} ∩ 𝑦) × ∪ dom
𝑃) = (∪ dom 𝑃 × ({0} ∩ 𝑦)) |
| 23 | 22 | dmeqi 5915 |
. . . . . 6
⊢ dom ◡(({0} ∩ 𝑦) × ∪ dom
𝑃) = dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) |
| 24 | 14, 21, 23 | 3eqtri 2769 |
. . . . 5
⊢ (◡(𝑥 ∈ ∪ dom
𝑃 ↦ 0) “ 𝑦) = dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) |
| 25 | | xpeq2 5706 |
. . . . . . . . . 10
⊢ (({0}
∩ 𝑦) = ∅ →
(∪ dom 𝑃 × ({0} ∩ 𝑦)) = (∪ dom 𝑃 ×
∅)) |
| 26 | | xp0 6178 |
. . . . . . . . . 10
⊢ (∪ dom 𝑃 × ∅) = ∅ |
| 27 | 25, 26 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (({0}
∩ 𝑦) = ∅ →
(∪ dom 𝑃 × ({0} ∩ 𝑦)) = ∅) |
| 28 | 27 | dmeqd 5916 |
. . . . . . . 8
⊢ (({0}
∩ 𝑦) = ∅ →
dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) = dom ∅) |
| 29 | | dm0 5931 |
. . . . . . . 8
⊢ dom
∅ = ∅ |
| 30 | 28, 29 | eqtrdi 2793 |
. . . . . . 7
⊢ (({0}
∩ 𝑦) = ∅ →
dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) = ∅) |
| 31 | 30 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) = ∅) |
| 32 | | 0rrv.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ Prob) |
| 33 | | domprobsiga 34413 |
. . . . . . . 8
⊢ (𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra) |
| 34 | | 0elsiga 34115 |
. . . . . . . 8
⊢ (dom
𝑃 ∈ ∪ ran sigAlgebra → ∅ ∈ dom 𝑃) |
| 35 | 32, 33, 34 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ∅ ∈ dom 𝑃) |
| 36 | 35 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → ∅
∈ dom 𝑃) |
| 37 | 31, 36 | eqeltrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) ∈ dom 𝑃) |
| 38 | 24, 37 | eqeltrid 2845 |
. . . 4
⊢ ((𝜑 ∧ ({0} ∩ 𝑦) = ∅) → (◡(𝑥 ∈ ∪ dom
𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃) |
| 39 | | dmxp 5939 |
. . . . . . 7
⊢ (({0}
∩ 𝑦) ≠ ∅
→ dom (∪ dom 𝑃 × ({0} ∩ 𝑦)) = ∪ dom 𝑃) |
| 40 | 39 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → dom
(∪ dom 𝑃 × ({0} ∩ 𝑦)) = ∪ dom 𝑃) |
| 41 | 32 | unveldomd 34417 |
. . . . . . 7
⊢ (𝜑 → ∪ dom 𝑃 ∈ dom 𝑃) |
| 42 | 41 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → ∪ dom 𝑃 ∈ dom 𝑃) |
| 43 | 40, 42 | eqeltrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → dom
(∪ dom 𝑃 × ({0} ∩ 𝑦)) ∈ dom 𝑃) |
| 44 | 24, 43 | eqeltrid 2845 |
. . . 4
⊢ ((𝜑 ∧ ({0} ∩ 𝑦) ≠ ∅) → (◡(𝑥 ∈ ∪ dom
𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃) |
| 45 | 38, 44 | pm2.61dane 3029 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ ∪ dom
𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃) |
| 46 | 45 | ralrimivw 3150 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝔅ℝ (◡(𝑥 ∈ ∪ dom
𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃) |
| 47 | 32 | isrrvv 34445 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ∪ dom
𝑃 ↦ 0) ∈
(rRndVar‘𝑃) ↔
((𝑥 ∈ ∪ dom 𝑃 ↦ 0):∪ dom
𝑃⟶ℝ ∧
∀𝑦 ∈
𝔅ℝ (◡(𝑥 ∈ ∪ dom 𝑃 ↦ 0) “ 𝑦) ∈ dom 𝑃))) |
| 48 | 6, 46, 47 | mpbir2and 713 |
1
⊢ (𝜑 → (𝑥 ∈ ∪ dom
𝑃 ↦ 0) ∈
(rRndVar‘𝑃)) |