Definition df-tsms 24426

Description: Define the set of limit points of an infinite group sum for the topological group 𝐺. If 𝐺 is Hausdorff, then there will be at most one element in this set and ∪ (𝑊 tsums 𝐹) selects this unique element if it exists. (𝑊 tsums 𝐹) ≈ 1_o is a way to say that the sum exists and is unique. Note that unlike Σ (df-sum 15834) and Σ_g (df-gsum 17593), this does not return the sum itself, but rather the set of all such sums, which is usually either empty or a singleton. (Contributed by Mario Carneiro, 2-Sep-2015.)

Assertion

Ref	Expression
df-tsms	⊢ tsums = (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋(𝒫 dom 𝑓 ∩ Fin) / 𝑠⦌(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})))‘(𝑦 ∈ 𝑠 ↦ (𝑤 Σg (𝑓 ↾ 𝑦)))))

Distinct variable group:   𝑓,𝑠,𝑤,𝑦,𝑧

Detailed syntax breakdown of Definition df-tsms

Step	Hyp	Ref	Expression
1		ctsu 24425	. 2 class tsums
2		vw	. . 3 setvar 𝑤
3		vf	. . 3 setvar 𝑓
4		cvv 3451	. . 3 class V
5		vs	. . . 4 setvar 𝑠
6	3	cv 1569	. . . . . . 7 class 𝑓
7	6	cdm 5651	. . . . . 6 class dom 𝑓
8	7	cpw 4557	. . . . 5 class 𝒫 dom 𝑓
9		cfn 8957	. . . . 5 class Fin
10	8, 9	cin 3898	. . . 4 class (𝒫 dom 𝑓 ∩ Fin)
11		vy	. . . . . 6 setvar 𝑦
12	5	cv 1569	. . . . . 6 class 𝑠
13	2	cv 1569	. . . . . . 7 class 𝑤
14	11	cv 1569	. . . . . . . 8 class 𝑦
15	6, 14	cres 5653	. . . . . . 7 class (𝑓 ↾ 𝑦)
16		cgsu 17591	. . . . . . 7 class Σg
17	13, 15, 16	co 7412	. . . . . 6 class (𝑤 Σg (𝑓 ↾ 𝑦))
18	11, 12, 17	cmpt 5186	. . . . 5 class (𝑦 ∈ 𝑠 ↦ (𝑤 Σg (𝑓 ↾ 𝑦)))
19		ctopn 17572	. . . . . . 7 class TopOpen
20	13, 19	cfv 6531	. . . . . 6 class (TopOpen‘𝑤)
21		vz	. . . . . . . . 9 setvar 𝑧
22	21	cv 1569	. . . . . . . . . . 11 class 𝑧
23	22, 14	wss 3899	. . . . . . . . . 10 wff 𝑧 ⊆ 𝑦
24	23, 11, 12	crab 3413	. . . . . . . . 9 class {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦}
25	21, 12, 24	cmpt 5186	. . . . . . . 8 class (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})
26	25	crn 5652	. . . . . . 7 class ran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})
27		cfg 21647	. . . . . . 7 class filGen
28	12, 26, 27	co 7412	. . . . . 6 class (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦}))
29		cflf 24234	. . . . . 6 class fLimf
30	20, 28, 29	co 7412	. . . . 5 class ((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})))
31	18, 30	cfv 6531	. . . 4 class (((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})))‘(𝑦 ∈ 𝑠 ↦ (𝑤 Σg (𝑓 ↾ 𝑦))))
32	5, 10, 31	csb 3847	. . 3 class ⦋(𝒫 dom 𝑓 ∩ Fin) / 𝑠⦌(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})))‘(𝑦 ∈ 𝑠 ↦ (𝑤 Σg (𝑓 ↾ 𝑦))))
33	2, 3, 4, 4, 32	cmpo 7414	. 2 class (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋(𝒫 dom 𝑓 ∩ Fin) / 𝑠⦌(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})))‘(𝑦 ∈ 𝑠 ↦ (𝑤 Σg (𝑓 ↾ 𝑦)))))
34	1, 33	wceq 1570	1 wff tsums = (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋(𝒫 dom 𝑓 ∩ Fin) / 𝑠⦌(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧 ∈ 𝑠 ↦ {𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦})))‘(𝑦 ∈ 𝑠 ↦ (𝑤 Σg (𝑓 ↾ 𝑦)))))

This definition is used by:  tsmsval2  24429