Step | Hyp | Ref
| Expression |
1 | | df-tsms 21930 |
. . 3
⊢ tsums =
(𝑤 ∈ V, 𝑓 ∈ V ↦
⦋(𝒫 dom 𝑓 ∩ Fin) / 𝑠⦌(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})))‘(𝑦 ∈ 𝑠 ↦ (𝑤 Σg (𝑓 ↾ 𝑦))))) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → tsums = (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋(𝒫
dom 𝑓 ∩ Fin) / 𝑠⦌(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})))‘(𝑦 ∈ 𝑠 ↦ (𝑤 Σg (𝑓 ↾ 𝑦)))))) |
3 | | vex 3203 |
. . . . . . 7
⊢ 𝑓 ∈ V |
4 | 3 | dmex 7099 |
. . . . . 6
⊢ dom 𝑓 ∈ V |
5 | 4 | pwex 4848 |
. . . . 5
⊢ 𝒫
dom 𝑓 ∈
V |
6 | 5 | inex1 4799 |
. . . 4
⊢
(𝒫 dom 𝑓
∩ Fin) ∈ V |
7 | 6 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) → (𝒫 dom 𝑓 ∩ Fin) ∈ V) |
8 | | simplrl 800 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → 𝑤 = 𝐺) |
9 | 8 | fveq2d 6195 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (TopOpen‘𝑤) = (TopOpen‘𝐺)) |
10 | | tsmsval.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) |
11 | 9, 10 | syl6eqr 2674 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (TopOpen‘𝑤) = 𝐽) |
12 | | id 22 |
. . . . . . 7
⊢ (𝑠 = (𝒫 dom 𝑓 ∩ Fin) → 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) |
13 | | simprr 796 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝑓 = 𝐹) |
14 | 13 | dmeqd 5326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) → dom 𝑓 = dom 𝐹) |
15 | | tsmsval2.a |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐹 = 𝐴) |
16 | 15 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) → dom 𝐹 = 𝐴) |
17 | 14, 16 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) → dom 𝑓 = 𝐴) |
18 | 17 | pweqd 4163 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝒫 dom 𝑓 = 𝒫 𝐴) |
19 | 18 | ineq1d 3813 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) → (𝒫 dom 𝑓 ∩ Fin) = (𝒫 𝐴 ∩ Fin)) |
20 | | tsmsval.s |
. . . . . . . 8
⊢ 𝑆 = (𝒫 𝐴 ∩ Fin) |
21 | 19, 20 | syl6eqr 2674 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) → (𝒫 dom 𝑓 ∩ Fin) = 𝑆) |
22 | 12, 21 | sylan9eqr 2678 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → 𝑠 = 𝑆) |
23 | | rabeq 3192 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
25 | 22, 24 | mpteq12dv 4733 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦}) = (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦})) |
26 | 25 | rneqd 5353 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → ran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦}) = ran (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦})) |
27 | | tsmsval.l |
. . . . . . 7
⊢ 𝐿 = ran (𝑧 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}) |
28 | 26, 27 | syl6eqr 2674 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → ran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦}) = 𝐿) |
29 | 22, 28 | oveq12d 6668 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})) = (𝑆filGen𝐿)) |
30 | 11, 29 | oveq12d 6668 |
. . . 4
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → ((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦}))) = (𝐽 fLimf (𝑆filGen𝐿))) |
31 | | simplrr 801 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → 𝑓 = 𝐹) |
32 | 31 | reseq1d 5395 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑓 ↾ 𝑦) = (𝐹 ↾ 𝑦)) |
33 | 8, 32 | oveq12d 6668 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑤 Σg (𝑓 ↾ 𝑦)) = (𝐺 Σg (𝐹 ↾ 𝑦))) |
34 | 22, 33 | mpteq12dv 4733 |
. . . 4
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (𝑦 ∈ 𝑠 ↦ (𝑤 Σg (𝑓 ↾ 𝑦))) = (𝑦 ∈ 𝑆 ↦ (𝐺 Σg (𝐹 ↾ 𝑦)))) |
35 | 30, 34 | fveq12d 6197 |
. . 3
⊢ (((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) ∧ 𝑠 = (𝒫 dom 𝑓 ∩ Fin)) → (((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})))‘(𝑦 ∈ 𝑠 ↦ (𝑤 Σg (𝑓 ↾ 𝑦)))) = ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦 ∈ 𝑆 ↦ (𝐺 Σg (𝐹 ↾ 𝑦))))) |
36 | 7, 35 | csbied 3560 |
. 2
⊢ ((𝜑 ∧ (𝑤 = 𝐺 ∧ 𝑓 = 𝐹)) → ⦋(𝒫 dom
𝑓 ∩ Fin) / 𝑠⦌(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})))‘(𝑦 ∈ 𝑠 ↦ (𝑤 Σg (𝑓 ↾ 𝑦)))) = ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦 ∈ 𝑆 ↦ (𝐺 Σg (𝐹 ↾ 𝑦))))) |
37 | | tsmsval.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
38 | | elex 3212 |
. . 3
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
39 | 37, 38 | syl 17 |
. 2
⊢ (𝜑 → 𝐺 ∈ V) |
40 | | tsmsval2.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑊) |
41 | | elex 3212 |
. . 3
⊢ (𝐹 ∈ 𝑊 → 𝐹 ∈ V) |
42 | 40, 41 | syl 17 |
. 2
⊢ (𝜑 → 𝐹 ∈ V) |
43 | | fvexd 6203 |
. 2
⊢ (𝜑 → ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦 ∈ 𝑆 ↦ (𝐺 Σg (𝐹 ↾ 𝑦)))) ∈ V) |
44 | 2, 36, 39, 42, 43 | ovmpt2d 6788 |
1
⊢ (𝜑 → (𝐺 tsums 𝐹) = ((𝐽 fLimf (𝑆filGen𝐿))‘(𝑦 ∈ 𝑆 ↦ (𝐺 Σg (𝐹 ↾ 𝑦))))) |