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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	eltsms.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
	eltsms.s	⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
	eltsms.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	eltsms.2	⊢ ( 𝜑 → 𝐺 ∈ TopSp )
	eltsms.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	eltsms.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	tsmsi.3	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐺 tsums 𝐹 ) )
	tsmsi.4	⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
	tsmsi.5	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
Assertion	tsmsi	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		eltsms.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		eltsms.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3		eltsms.s	⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
4		eltsms.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
5		eltsms.2	⊢ ( 𝜑 → 𝐺 ∈ TopSp )
6		eltsms.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7		eltsms.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8		tsmsi.3	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐺 tsums 𝐹 ) )
9		tsmsi.4	⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
10		tsmsi.5	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
11		eleq2	⊢ ( 𝑢 = 𝑈 → ( 𝐶 ∈ 𝑢 ↔ 𝐶 ∈ 𝑈 ) )
12		eleq2	⊢ ( 𝑢 = 𝑈 → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑈 ) )
13	12	imbi2d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ↔ ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑈 ) ) )
14	13	rexralbidv	⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ↔ ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑈 ) ) )
15	11 14	imbi12d	⊢ ( 𝑢 = 𝑈 → ( ( 𝐶 ∈ 𝑢 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ↔ ( 𝐶 ∈ 𝑈 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑈 ) ) ) )
16	1 2 3 4 5 6 7	eltsms	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐺 tsums 𝐹 ) ↔ ( 𝐶 ∈ 𝐵 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝐶 ∈ 𝑢 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) ) )
17	8 16	mpbid	⊢ ( 𝜑 → ( 𝐶 ∈ 𝐵 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝐶 ∈ 𝑢 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) )
18	17	simprd	⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐽 ( 𝐶 ∈ 𝑢 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) )
19	15 18 9	rspcdva	⊢ ( 𝜑 → ( 𝐶 ∈ 𝑈 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑈 ) ) )
20	10 19	mpd	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑈 ) )