Step | Hyp | Ref
| Expression |
1 | | tsmssubm.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) |
2 | | tsmssubm.h |
. . . . . . 7
⊢ 𝐻 = (𝐺 ↾s 𝑆) |
3 | 2 | submbas 17355 |
. . . . . 6
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝑆 = (Base‘𝐻)) |
4 | 1, 3 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 = (Base‘𝐻)) |
5 | 4 | eleq2d 2687 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ (Base‘𝐻))) |
6 | 5 | anbi1d 741 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ∧ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣))) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣))))) |
7 | | elin 3796 |
. . . . 5
⊢ (𝑥 ∈ ((𝐺 tsums 𝐹) ∩ 𝑆) ↔ (𝑥 ∈ (𝐺 tsums 𝐹) ∧ 𝑥 ∈ 𝑆)) |
8 | | ancom 466 |
. . . . 5
⊢ ((𝑥 ∈ (𝐺 tsums 𝐹) ∧ 𝑥 ∈ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝐺 tsums 𝐹))) |
9 | 7, 8 | bitri 264 |
. . . 4
⊢ (𝑥 ∈ ((𝐺 tsums 𝐹) ∩ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝐺 tsums 𝐹))) |
10 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Base‘𝐺) =
(Base‘𝐺) |
11 | 10 | submss 17350 |
. . . . . . . . 9
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
12 | 1, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝐺)) |
13 | 12 | sselda 3603 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝐺)) |
14 | | eqid 2622 |
. . . . . . . . 9
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) |
15 | | eqid 2622 |
. . . . . . . . 9
⊢
(𝒫 𝐴 ∩
Fin) = (𝒫 𝐴 ∩
Fin) |
16 | | tsmssubm.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ CMnd) |
17 | | tsmssubm.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ TopSp) |
18 | | tsmssubm.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
19 | | tsmssubm.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
20 | 19, 12 | fssd 6057 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝐺)) |
21 | 10, 14, 15, 16, 17, 18, 20 | eltsms 21936 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥 ∈ (Base‘𝐺) ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))))) |
22 | 21 | baibd 948 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) |
23 | 13, 22 | syldan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) |
24 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑢 ∈ V |
25 | 24 | inex1 4799 |
. . . . . . . 8
⊢ (𝑢 ∩ 𝑆) ∈ V |
26 | 25 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑢 ∈ (TopOpen‘𝐺)) → (𝑢 ∩ 𝑆) ∈ V) |
27 | 2, 14 | resstopn 20990 |
. . . . . . . . 9
⊢
((TopOpen‘𝐺)
↾t 𝑆) =
(TopOpen‘𝐻) |
28 | 27 | eleq2i 2693 |
. . . . . . . 8
⊢ (𝑣 ∈ ((TopOpen‘𝐺) ↾t 𝑆) ↔ 𝑣 ∈ (TopOpen‘𝐻)) |
29 | | fvex 6201 |
. . . . . . . . . 10
⊢
(TopOpen‘𝐺)
∈ V |
30 | | elrest 16088 |
. . . . . . . . . 10
⊢
(((TopOpen‘𝐺)
∈ V ∧ 𝑆 ∈
(SubMnd‘𝐺)) →
(𝑣 ∈
((TopOpen‘𝐺)
↾t 𝑆)
↔ ∃𝑢 ∈
(TopOpen‘𝐺)𝑣 = (𝑢 ∩ 𝑆))) |
31 | 29, 1, 30 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ ((TopOpen‘𝐺) ↾t 𝑆) ↔ ∃𝑢 ∈ (TopOpen‘𝐺)𝑣 = (𝑢 ∩ 𝑆))) |
32 | 31 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑣 ∈ ((TopOpen‘𝐺) ↾t 𝑆) ↔ ∃𝑢 ∈ (TopOpen‘𝐺)𝑣 = (𝑢 ∩ 𝑆))) |
33 | 28, 32 | syl5bbr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑣 ∈ (TopOpen‘𝐻) ↔ ∃𝑢 ∈ (TopOpen‘𝐺)𝑣 = (𝑢 ∩ 𝑆))) |
34 | | eleq2 2690 |
. . . . . . . . 9
⊢ (𝑣 = (𝑢 ∩ 𝑆) → (𝑥 ∈ 𝑣 ↔ 𝑥 ∈ (𝑢 ∩ 𝑆))) |
35 | | elin 3796 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑢 ∩ 𝑆) ↔ (𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑆)) |
36 | 35 | rbaib 947 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑆 → (𝑥 ∈ (𝑢 ∩ 𝑆) ↔ 𝑥 ∈ 𝑢)) |
37 | 36 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (𝑢 ∩ 𝑆) ↔ 𝑥 ∈ 𝑢)) |
38 | 34, 37 | sylan9bbr 737 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) → (𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝑢)) |
39 | | eleq2 2690 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑢 ∩ 𝑆) → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣 ↔ (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ (𝑢 ∩ 𝑆))) |
40 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝐻) =
(Base‘𝐻) |
41 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘𝐻) = (0g‘𝐻) |
42 | 2 | submmnd 17354 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝐻 ∈ Mnd) |
43 | 1, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐻 ∈ Mnd) |
44 | 2 | subcmn 18242 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ CMnd ∧ 𝐻 ∈ Mnd) → 𝐻 ∈ CMnd) |
45 | 16, 43, 44 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐻 ∈ CMnd) |
46 | 45 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐻 ∈ CMnd) |
47 | | elfpw 8268 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin)) |
48 | 47 | simprbi 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin) |
50 | 19 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐴⟶𝑆) |
51 | 47 | simplbi 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴) |
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴) |
53 | 50, 52 | fssresd 6071 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑦):𝑦⟶𝑆) |
54 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑆 = (Base‘𝐻)) |
55 | 54 | feq3d 6032 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ 𝑦):𝑦⟶𝑆 ↔ (𝐹 ↾ 𝑦):𝑦⟶(Base‘𝐻))) |
56 | 53, 55 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑦):𝑦⟶(Base‘𝐻)) |
57 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0g‘𝐻) ∈ V |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) →
(0g‘𝐻)
∈ V) |
59 | 53, 49, 58 | fdmfifsupp 8285 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑦) finSupp (0g‘𝐻)) |
60 | 40, 41, 46, 49, 56, 59 | gsumcl 18316 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ (Base‘𝐻)) |
61 | 60, 54 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑆) |
62 | | elin 3796 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻 Σg
(𝐹 ↾ 𝑦)) ∈ (𝑢 ∩ 𝑆) ↔ ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢 ∧ (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑆)) |
63 | 62 | rbaib 947 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 Σg
(𝐹 ↾ 𝑦)) ∈ 𝑆 → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ (𝑢 ∩ 𝑆) ↔ (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) |
64 | 61, 63 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ (𝑢 ∩ 𝑆) ↔ (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) |
65 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑆 ∈ (SubMnd‘𝐺)) |
66 | 49, 65, 53, 2 | gsumsubm 17373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑦)) = (𝐻 Σg (𝐹 ↾ 𝑦))) |
67 | 66 | eleq1d 2686 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢 ↔ (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) |
68 | 64, 67 | bitr4d 271 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ (𝑢 ∩ 𝑆) ↔ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) |
69 | 39, 68 | sylan9bbr 737 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑣 = (𝑢 ∩ 𝑆)) → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣 ↔ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) |
70 | 69 | an32s 846 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣 ↔ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) |
71 | 70 | imbi2d 330 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) ↔ (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))) |
72 | 71 | ralbidva 2985 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) → (∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))) |
73 | 72 | rexbidv 3052 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) → (∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))) |
74 | 38, 73 | imbi12d 334 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑣 = (𝑢 ∩ 𝑆)) → ((𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣)) ↔ (𝑥 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) |
75 | 26, 33, 74 | ralxfr2d 4882 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣)) ↔ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) |
76 | 23, 75 | bitr4d 271 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣)))) |
77 | 76 | pm5.32da 673 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ∧ 𝑥 ∈ (𝐺 tsums 𝐹)) ↔ (𝑥 ∈ 𝑆 ∧ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣))))) |
78 | 9, 77 | syl5bb 272 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐺 tsums 𝐹) ∩ 𝑆) ↔ (𝑥 ∈ 𝑆 ∧ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣))))) |
79 | | eqid 2622 |
. . . 4
⊢
(TopOpen‘𝐻) =
(TopOpen‘𝐻) |
80 | | resstps 20991 |
. . . . . 6
⊢ ((𝐺 ∈ TopSp ∧ 𝑆 ∈ (SubMnd‘𝐺)) → (𝐺 ↾s 𝑆) ∈ TopSp) |
81 | 17, 1, 80 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾s 𝑆) ∈ TopSp) |
82 | 2, 81 | syl5eqel 2705 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ TopSp) |
83 | 4 | feq3d 6032 |
. . . . 5
⊢ (𝜑 → (𝐹:𝐴⟶𝑆 ↔ 𝐹:𝐴⟶(Base‘𝐻))) |
84 | 19, 83 | mpbid 222 |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝐻)) |
85 | 40, 79, 15, 45, 82, 18, 84 | eltsms 21936 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐻 tsums 𝐹) ↔ (𝑥 ∈ (Base‘𝐻) ∧ ∀𝑣 ∈ (TopOpen‘𝐻)(𝑥 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐻 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣))))) |
86 | 6, 78, 85 | 3bitr4rd 301 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐻 tsums 𝐹) ↔ 𝑥 ∈ ((𝐺 tsums 𝐹) ∩ 𝑆))) |
87 | 86 | eqrdv 2620 |
1
⊢ (𝜑 → (𝐻 tsums 𝐹) = ((𝐺 tsums 𝐹) ∩ 𝑆)) |