| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tsmssubm.s | . . . . . 6
⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) | 
| 2 |  | tsmssubm.h | . . . . . . 7
⊢ 𝐻 = (𝐺 ↾s 𝑆) | 
| 3 | 2 | submbas 18827 | . . . . . 6
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝑆 = (Base‘𝐻)) | 
| 4 | 1, 3 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑆 = (Base‘𝐻)) | 
| 5 | 4 | eleq2d 2827 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ (Base‘𝐻))) | 
| 6 | 5 | anbi1d 631 | . . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ∧ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣))) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣))))) | 
| 7 |  | elin 3967 | . . . . 5
⊢ (𝑥 ∈ ((𝐺 tsums 𝐹) ∩ 𝑆) ↔ (𝑥 ∈ (𝐺 tsums 𝐹) ∧ 𝑥 ∈ 𝑆)) | 
| 8 | 7 | biancomi 462 | . . . 4
⊢ (𝑥 ∈ ((𝐺 tsums 𝐹) ∩ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝐺 tsums 𝐹))) | 
| 9 |  | eqid 2737 | . . . . . . . . . 10
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 10 | 9 | submss 18822 | . . . . . . . . 9
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) | 
| 11 | 1, 10 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝐺)) | 
| 12 | 11 | sselda 3983 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝐺)) | 
| 13 |  | eqid 2737 | . . . . . . . . 9
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) | 
| 14 |  | eqid 2737 | . . . . . . . . 9
⊢
(𝒫 𝐴 ∩
Fin) = (𝒫 𝐴 ∩
Fin) | 
| 15 |  | tsmssubm.1 | . . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ CMnd) | 
| 16 |  | tsmssubm.2 | . . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ TopSp) | 
| 17 |  | tsmssubm.a | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 18 |  | tsmssubm.f | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) | 
| 19 | 18, 11 | fssd 6753 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝐺)) | 
| 20 | 9, 13, 14, 15, 16, 17, 19 | eltsms 24141 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))))) | 
| 21 | 20 | baibd 539 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) | 
| 22 | 12, 21 | syldan 591 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) | 
| 23 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑢 ∈ V | 
| 24 | 23 | inex1 5317 | . . . . . . . 8
⊢ (𝑢 ∩ 𝑆) ∈ V | 
| 25 | 24 | a1i 11 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑢 ∈ (TopOpen‘𝐺)) → (𝑢 ∩ 𝑆) ∈ V) | 
| 26 | 2, 13 | resstopn 23194 | . . . . . . . . 9
⊢
((TopOpen‘𝐺)
↾t 𝑆) =
(TopOpen‘𝐻) | 
| 27 | 26 | eleq2i 2833 | . . . . . . . 8
⊢ (𝑣 ∈ ((TopOpen‘𝐺) ↾t 𝑆) ↔ 𝑣 ∈ (TopOpen‘𝐻)) | 
| 28 |  | fvex 6919 | . . . . . . . . . 10
⊢
(TopOpen‘𝐺)
∈ V | 
| 29 |  | elrest 17472 | . . . . . . . . . 10
⊢
(((TopOpen‘𝐺)
∈ V ∧ 𝑆 ∈
(SubMnd‘𝐺)) →
(𝑣 ∈
((TopOpen‘𝐺)
↾t 𝑆)
↔ ∃𝑢 ∈
(TopOpen‘𝐺)𝑣 = (𝑢 ∩ 𝑆))) | 
| 30 | 28, 1, 29 | sylancr 587 | . . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ ((TopOpen‘𝐺) ↾t 𝑆) ↔ ∃𝑢 ∈ (TopOpen‘𝐺)𝑣 = (𝑢 ∩ 𝑆))) | 
| 31 | 30 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑣 ∈ ((TopOpen‘𝐺) ↾t 𝑆) ↔ ∃𝑢 ∈ (TopOpen‘𝐺)𝑣 = (𝑢 ∩ 𝑆))) | 
| 32 | 27, 31 | bitr3id 285 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑣 ∈ (TopOpen‘𝐻) ↔ ∃𝑢 ∈ (TopOpen‘𝐺)𝑣 = (𝑢 ∩ 𝑆))) | 
| 33 |  | eleq2 2830 | . . . . . . . . 9
⊢ (𝑣 = (𝑢 ∩ 𝑆) → (𝑥 ∈ 𝑣 ↔ 𝑥 ∈ (𝑢 ∩ 𝑆))) | 
| 34 |  | elin 3967 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑢 ∩ 𝑆) ↔ (𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑆)) | 
| 35 | 34 | rbaib 538 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝑆 → (𝑥 ∈ (𝑢 ∩ 𝑆) ↔ 𝑥 ∈ 𝑢)) | 
| 36 | 35 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (𝑢 ∩ 𝑆) ↔ 𝑥 ∈ 𝑢)) | 
| 37 | 33, 36 | sylan9bbr 510 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) → (𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝑢)) | 
| 38 |  | eleq2 2830 | . . . . . . . . . . . . 13
⊢ (𝑣 = (𝑢 ∩ 𝑆) → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣 ↔ (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ (𝑢 ∩ 𝑆))) | 
| 39 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 40 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢
(0g‘𝐻) = (0g‘𝐻) | 
| 41 | 2 | submmnd 18826 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝐻 ∈ Mnd) | 
| 42 | 1, 41 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐻 ∈ Mnd) | 
| 43 | 2 | subcmn 19855 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ CMnd ∧ 𝐻 ∈ Mnd) → 𝐻 ∈ CMnd) | 
| 44 | 15, 42, 43 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐻 ∈ CMnd) | 
| 45 | 44 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐻 ∈ CMnd) | 
| 46 |  | elinel2 4202 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin) | 
| 47 | 46 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin) | 
| 48 | 18 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐴⟶𝑆) | 
| 49 |  | elfpw 9394 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin)) | 
| 50 | 49 | simplbi 497 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴) | 
| 51 | 50 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴) | 
| 52 | 48, 51 | fssresd 6775 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑦):𝑦⟶𝑆) | 
| 53 | 4 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑆 = (Base‘𝐻)) | 
| 54 | 53 | feq3d 6723 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ 𝑦):𝑦⟶𝑆 ↔ (𝐹 ↾ 𝑦):𝑦⟶(Base‘𝐻))) | 
| 55 | 52, 54 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑦):𝑦⟶(Base‘𝐻)) | 
| 56 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . 19
⊢
(0g‘𝐻) ∈ V | 
| 57 | 56 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) →
(0g‘𝐻)
∈ V) | 
| 58 | 52, 47, 57 | fdmfifsupp 9415 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑦) finSupp (0g‘𝐻)) | 
| 59 | 39, 40, 45, 47, 55, 58 | gsumcl 19933 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ (Base‘𝐻)) | 
| 60 | 59, 53 | eleqtrrd 2844 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑆) | 
| 61 |  | elin 3967 | . . . . . . . . . . . . . . . 16
⊢ ((𝐻 Σg
(𝐹 ↾ 𝑦)) ∈ (𝑢 ∩ 𝑆) ↔ ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢 ∧ (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑆)) | 
| 62 | 61 | rbaib 538 | . . . . . . . . . . . . . . 15
⊢ ((𝐻 Σg
(𝐹 ↾ 𝑦)) ∈ 𝑆 → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ (𝑢 ∩ 𝑆) ↔ (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) | 
| 63 | 60, 62 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ (𝑢 ∩ 𝑆) ↔ (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) | 
| 64 | 1 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑆 ∈ (SubMnd‘𝐺)) | 
| 65 | 47, 64, 52, 2 | gsumsubm 18848 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑦)) = (𝐻 Σg (𝐹 ↾ 𝑦))) | 
| 66 | 65 | eleq1d 2826 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢 ↔ (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) | 
| 67 | 63, 66 | bitr4d 282 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ (𝑢 ∩ 𝑆) ↔ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) | 
| 68 | 38, 67 | sylan9bbr 510 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑣 = (𝑢 ∩ 𝑆)) → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣 ↔ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) | 
| 69 | 68 | an32s 652 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣 ↔ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) | 
| 70 | 69 | imbi2d 340 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) ↔ (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))) | 
| 71 | 70 | ralbidva 3176 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) → (∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))) | 
| 72 | 71 | rexbidv 3179 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) → (∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))) | 
| 73 | 37, 72 | imbi12d 344 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) → ((𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣)) ↔ (𝑥 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) | 
| 74 | 25, 32, 73 | ralxfr2d 5410 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣)) ↔ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) | 
| 75 | 22, 74 | bitr4d 282 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣)))) | 
| 76 | 75 | pm5.32da 579 | . . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ↔ (𝑥 ∈ 𝑆 ∧ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣))))) | 
| 77 | 8, 76 | bitrid 283 | . . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐺 tsums 𝐹) ∩ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣))))) | 
| 78 |  | eqid 2737 | . . . 4
⊢
(TopOpen‘𝐻) =
(TopOpen‘𝐻) | 
| 79 |  | resstps 23195 | . . . . . 6
⊢ ((𝐺 ∈ TopSp ∧ 𝑆 ∈ (SubMnd‘𝐺)) → (𝐺 ↾s 𝑆) ∈ TopSp) | 
| 80 | 16, 1, 79 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐺 ↾s 𝑆) ∈ TopSp) | 
| 81 | 2, 80 | eqeltrid 2845 | . . . 4
⊢ (𝜑 → 𝐻 ∈ TopSp) | 
| 82 | 4 | feq3d 6723 | . . . . 5
⊢ (𝜑 → (𝐹:𝐴⟶𝑆 ↔ 𝐹:𝐴⟶(Base‘𝐻))) | 
| 83 | 18, 82 | mpbid 232 | . . . 4
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝐻)) | 
| 84 | 39, 78, 14, 44, 81, 17, 83 | eltsms 24141 | . . 3
⊢ (𝜑 → (𝑥 ∈ (𝐻 tsums 𝐹) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣))))) | 
| 85 | 6, 77, 84 | 3bitr4rd 312 | . 2
⊢ (𝜑 → (𝑥 ∈ (𝐻 tsums 𝐹) ↔ 𝑥 ∈ ((𝐺 tsums 𝐹) ∩ 𝑆))) | 
| 86 | 85 | eqrdv 2735 | 1
⊢ (𝜑 → (𝐻 tsums 𝐹) = ((𝐺 tsums 𝐹) ∩ 𝑆)) |