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

Metamath Proof Explorer

Theorem tsmsgsum

Description: The convergent points of a finite topological group sum are the closure of the finite group sum operation. (Contributed by Mario Carneiro, 19-Sep-2015) (Revised by AV, 24-Jul-2019)

Ref Expression
Hypotheses tsmsid.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmsid.z ⊢ 0 = ( 0g ‘ 𝐺 )
tsmsid.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmsid.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
tsmsid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmsid.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
tsmsid.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
tsmsgsum.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion tsmsgsum ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( cls ‘ 𝐽 ) ‘ { ( 𝐺 Σg 𝐹 ) } ) )

Proof

Step Hyp Ref Expression
1 tsmsid.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tsmsid.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 tsmsid.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 tsmsid.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
5 tsmsid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 tsmsid.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 tsmsid.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
8 tsmsgsum.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
9 1 8 istps ⊢ ( 𝐺 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
10 4 9 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
11 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = ∪ 𝐽 )
12 10 11 syl ⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 )
13 12 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ∪ 𝐽 ) )
14 elfpw ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin ) )
15 14 simplbi ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
16 15 adantl ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ⊆ 𝐴 )
17 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
18 17 6 fssdm ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐴 )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 supp 0 ) ⊆ 𝐴 )
20 16 19 unssd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ⊆ 𝐴 )
21 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin )
22 21 adantl ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ Fin )
23 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 finSupp 0 )
24 23 fsuppimpd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 supp 0 ) ∈ Fin )
25 unfi ⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝐹 supp 0 ) ∈ Fin ) → ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ∈ Fin )
26 22 24 25 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ∈ Fin )
27 elfpw ⊢ ( ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ⊆ 𝐴 ∧ ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ∈ Fin ) )
28 20 26 27 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
29 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ ( 𝐹 supp 0 ) )
30 id ⊢ ( 𝑧 = ( 𝑦 ∪ ( 𝐹 supp 0 ) ) → 𝑧 = ( 𝑦 ∪ ( 𝐹 supp 0 ) ) )
31 29 30 sseqtrrid ⊢ ( 𝑧 = ( 𝑦 ∪ ( 𝐹 supp 0 ) ) → 𝑦 ⊆ 𝑧 )
32 pm5.5 ⊢ ( 𝑦 ⊆ 𝑧 → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
33 31 32 syl ⊢ ( 𝑧 = ( 𝑦 ∪ ( 𝐹 supp 0 ) ) → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
34 reseq2 ⊢ ( 𝑧 = ( 𝑦 ∪ ( 𝐹 supp 0 ) ) → ( 𝐹 ↾ 𝑧 ) = ( 𝐹 ↾ ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ) )
35 34 oveq2d ⊢ ( 𝑧 = ( 𝑦 ∪ ( 𝐹 supp 0 ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ) ) )
36 35 eleq1d ⊢ ( 𝑧 = ( 𝑦 ∪ ( 𝐹 supp 0 ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ) ) ∈ 𝑢 ) )
37 33 36 bitrd ⊢ ( 𝑧 = ( 𝑦 ∪ ( 𝐹 supp 0 ) ) → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ) ) ∈ 𝑢 ) )
38 37 rspcv ⊢ ( ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ) ) ∈ 𝑢 ) )
39 28 38 syl ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ) ) ∈ 𝑢 ) )
40 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐺 ∈ CMnd )
41 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐴 ∈ 𝑉 )
42 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
43 ssun2 ⊢ ( 𝐹 supp 0 ) ⊆ ( 𝑦 ∪ ( 𝐹 supp 0 ) )
44 43 a1i ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 supp 0 ) ⊆ ( 𝑦 ∪ ( 𝐹 supp 0 ) ) )
45 1 2 40 41 42 44 23 gsumres ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ) ) = ( 𝐺 Σg 𝐹 ) )
46 45 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ ( 𝐹 supp 0 ) ) ) ) ∈ 𝑢 ↔ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) )
47 39 46 sylibd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) )
48 47 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) )
49 7 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
50 elfpw ⊢ ( ( 𝐹 supp 0 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ( 𝐹 supp 0 ) ⊆ 𝐴 ∧ ( 𝐹 supp 0 ) ∈ Fin ) )
51 18 49 50 sylanbrc ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
52 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝐹 supp 0 ) ⊆ 𝑧 ) ) → 𝐺 ∈ CMnd )
53 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝐹 supp 0 ) ⊆ 𝑧 ) ) → 𝐴 ∈ 𝑉 )
54 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝐹 supp 0 ) ⊆ 𝑧 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
55 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝐹 supp 0 ) ⊆ 𝑧 ) ) → ( 𝐹 supp 0 ) ⊆ 𝑧 )
56 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝐹 supp 0 ) ⊆ 𝑧 ) ) → 𝐹 finSupp 0 )
57 1 2 52 53 54 55 56 gsumres ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝐹 supp 0 ) ⊆ 𝑧 ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) = ( 𝐺 Σg 𝐹 ) )
58 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝐹 supp 0 ) ⊆ 𝑧 ) ) → ( 𝐺 Σg 𝐹 ) ∈ 𝑢 )
59 57 58 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝐹 supp 0 ) ⊆ 𝑧 ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 )
60 59 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 supp 0 ) ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
61 60 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) ) → ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( 𝐹 supp 0 ) ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
62 sseq1 ⊢ ( 𝑦 = ( 𝐹 supp 0 ) → ( 𝑦 ⊆ 𝑧 ↔ ( 𝐹 supp 0 ) ⊆ 𝑧 ) )
63 62 rspceaimv ⊢ ( ( ( 𝐹 supp 0 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( 𝐹 supp 0 ) ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
64 51 61 63 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
65 64 expr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ( ( 𝐺 Σg 𝐹 ) ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
66 48 65 impbid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ) )
67 disjsn ⊢ ( ( 𝑢 ∩ { ( 𝐺 Σg 𝐹 ) } ) = ∅ ↔ ¬ ( 𝐺 Σg 𝐹 ) ∈ 𝑢 )
68 67 necon2abii ⊢ ( ( 𝐺 Σg 𝐹 ) ∈ 𝑢 ↔ ( 𝑢 ∩ { ( 𝐺 Σg 𝐹 ) } ) ≠ ∅ )
69 66 68 bitrdi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝑢 ∩ { ( 𝐺 Σg 𝐹 ) } ) ≠ ∅ ) )
70 69 imbi2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ↔ ( 𝑥 ∈ 𝑢 → ( 𝑢 ∩ { ( 𝐺 Σg 𝐹 ) } ) ≠ ∅ ) ) )
71 70 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ( 𝑢 ∩ { ( 𝐺 Σg 𝐹 ) } ) ≠ ∅ ) ) )
72 13 71 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ( 𝑢 ∩ { ( 𝐺 Σg 𝐹 ) } ) ≠ ∅ ) ) ) )
73 eqid ⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
74 1 8 73 3 4 5 6 eltsms ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ) )
75 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐽 ∈ Top )
76 10 75 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
77 1 2 3 5 6 7 gsumcl ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 )
78 77 snssd ⊢ ( 𝜑 → { ( 𝐺 Σg 𝐹 ) } ⊆ 𝐵 )
79 78 12 sseqtrd ⊢ ( 𝜑 → { ( 𝐺 Σg 𝐹 ) } ⊆ ∪ 𝐽 )
80 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
81 80 elcls2 ⊢ ( ( 𝐽 ∈ Top ∧ { ( 𝐺 Σg 𝐹 ) } ⊆ ∪ 𝐽 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { ( 𝐺 Σg 𝐹 ) } ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ( 𝑢 ∩ { ( 𝐺 Σg 𝐹 ) } ) ≠ ∅ ) ) ) )
82 76 79 81 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { ( 𝐺 Σg 𝐹 ) } ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ( 𝑢 ∩ { ( 𝐺 Σg 𝐹 ) } ) ≠ ∅ ) ) ) )
83 72 74 82 3bitr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ { ( 𝐺 Σg 𝐹 ) } ) ) )
84 83 eqrdv ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( cls ‘ 𝐽 ) ‘ { ( 𝐺 Σg 𝐹 ) } ) )