This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tsmsi

Description: The property of being a sum of the sequence F in the topological commutative monoid G . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses eltsms.b ⊢ B = Base G
eltsms.j ⊢ J = TopOpen ⁡ G
eltsms.s ⊢ S = 𝒫 A ∩ Fin
eltsms.1 ⊢ φ → G ∈ CMnd
eltsms.2 ⊢ φ → G ∈ TopSp
eltsms.a ⊢ φ → A ∈ V
eltsms.f ⊢ φ → F : A ⟶ B
tsmsi.3 ⊢ φ → C ∈ G tsums F
tsmsi.4 ⊢ φ → U ∈ J
tsmsi.5 ⊢ φ → C ∈ U
Assertion tsmsi ⊢ φ → ∃ z ∈ S ∀ y ∈ S z ⊆ y → ∑ G F ↾ y ∈ U

Proof

Step Hyp Ref Expression
1 eltsms.b ⊢ B = Base G
2 eltsms.j ⊢ J = TopOpen ⁡ G
3 eltsms.s ⊢ S = 𝒫 A ∩ Fin
4 eltsms.1 ⊢ φ → G ∈ CMnd
5 eltsms.2 ⊢ φ → G ∈ TopSp
6 eltsms.a ⊢ φ → A ∈ V
7 eltsms.f ⊢ φ → F : A ⟶ B
8 tsmsi.3 ⊢ φ → C ∈ G tsums F
9 tsmsi.4 ⊢ φ → U ∈ J
10 tsmsi.5 ⊢ φ → C ∈ U
11 eleq2 ⊢ u = U → C ∈ u ↔ C ∈ U
12 eleq2 ⊢ u = U → ∑ G F ↾ y ∈ u ↔ ∑ G F ↾ y ∈ U
13 12 imbi2d ⊢ u = U → z ⊆ y → ∑ G F ↾ y ∈ u ↔ z ⊆ y → ∑ G F ↾ y ∈ U
14 13 rexralbidv ⊢ u = U → ∃ z ∈ S ∀ y ∈ S z ⊆ y → ∑ G F ↾ y ∈ u ↔ ∃ z ∈ S ∀ y ∈ S z ⊆ y → ∑ G F ↾ y ∈ U
15 11 14 imbi12d ⊢ u = U → C ∈ u → ∃ z ∈ S ∀ y ∈ S z ⊆ y → ∑ G F ↾ y ∈ u ↔ C ∈ U → ∃ z ∈ S ∀ y ∈ S z ⊆ y → ∑ G F ↾ y ∈ U
16 1 2 3 4 5 6 7 eltsms ⊢ φ → C ∈ G tsums F ↔ C ∈ B ∧ ∀ u ∈ J C ∈ u → ∃ z ∈ S ∀ y ∈ S z ⊆ y → ∑ G F ↾ y ∈ u
17 8 16 mpbid ⊢ φ → C ∈ B ∧ ∀ u ∈ J C ∈ u → ∃ z ∈ S ∀ y ∈ S z ⊆ y → ∑ G F ↾ y ∈ u
18 17 simprd ⊢ φ → ∀ u ∈ J C ∈ u → ∃ z ∈ S ∀ y ∈ S z ⊆ y → ∑ G F ↾ y ∈ u
19 15 18 9 rspcdva ⊢ φ → C ∈ U → ∃ z ∈ S ∀ y ∈ S z ⊆ y → ∑ G F ↾ y ∈ U
20 10 19 mpd ⊢ φ → ∃ z ∈ S ∀ y ∈ S z ⊆ y → ∑ G F ↾ y ∈ U