tsmsxp

Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 for the main proof; this part mostly sets up the local assumptions. (Contributed by Mario Carneiro, 21-Sep-2015)

	Ref	Expression
Hypotheses	tsmsxp.b	$⊢ B = {Base}_{G}$
	tsmsxp.g	$⊢ φ \to G \in CMnd$
	tsmsxp.2	$⊢ φ \to G \in TopGrp$
	tsmsxp.a	$⊢ φ \to A \in V$
	tsmsxp.c	$⊢ φ \to C \in W$
	tsmsxp.f	$⊢ φ \to F : A \times C ⟶ B$
	tsmsxp.h	$⊢ φ \to H : A ⟶ B$
	tsmsxp.1	$⊢ (φ \land j \in A) \to H (j) \in (G tsums (k \in C ⟼ j F k))$
Assertion	tsmsxp	$⊢ φ \to G tsums F \subseteq G tsums H$

Proof

Step	Hyp	Ref	Expression
1		tsmsxp.b	$⊢ B = {Base}_{G}$
2		tsmsxp.g	$⊢ φ \to G \in CMnd$
3		tsmsxp.2	$⊢ φ \to G \in TopGrp$
4		tsmsxp.a	$⊢ φ \to A \in V$
5		tsmsxp.c	$⊢ φ \to C \in W$
6		tsmsxp.f	$⊢ φ \to F : A \times C ⟶ B$
7		tsmsxp.h	$⊢ φ \to H : A ⟶ B$
8		tsmsxp.1	$⊢ (φ \land j \in A) \to H (j) \in (G tsums (k \in C ⟼ j F k))$
9		tgptmd	$⊢ G \in TopGrp \to G \in TopMnd$
10	3 9	syl	$⊢ φ \to G \in TopMnd$
11	10	3ad2ant1	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to G \in TopMnd$
12		simp2	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to u \in TopOpen (G)$
13		eqid	$⊢ TopOpen (G) = TopOpen (G)$
14	13 1	tmdtopon	$⊢ G \in TopMnd \to TopOpen (G) \in TopOn (B)$
15	11 14	syl	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to TopOpen (G) \in TopOn (B)$
16		toponss	$⊢ (TopOpen (G) \in TopOn (B) \land u \in TopOpen (G)) \to u \subseteq B$
17	15 12 16	syl2anc	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to u \subseteq B$
18		simp3	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to x \in u$
19	17 18	sseldd	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to x \in B$
20		tmdmnd	$⊢ G \in TopMnd \to G \in Mnd$
21	11 20	syl	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to G \in Mnd$
22		eqid	$⊢ 0_{G} = 0_{G}$
23	1 22	mndidcl	$⊢ G \in Mnd \to 0_{G} \in B$
24	21 23	syl	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to 0_{G} \in B$
25		eqid	$⊢ +_{G} = +_{G}$
26	1 25 22	mndrid	$⊢ (G \in Mnd \land x \in B) \to x +_{G} 0_{G} = x$
27	21 19 26	syl2anc	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to x +_{G} 0_{G} = x$
28	27 18	eqeltrd	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to x +_{G} 0_{G} \in u$
29	1 13 25	tmdcn2	$⊢ ((G \in TopMnd \land u \in TopOpen (G)) \land (x \in B \land 0_{G} \in B \land x +_{G} 0_{G} \in u)) \to \exists v \in TopOpen (G) \exists t \in TopOpen (G) (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)$
30	11 12 19 24 28 29	syl23anc	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to \exists v \in TopOpen (G) \exists t \in TopOpen (G) (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)$
31		r19.29	$⊢ (\forall v \in TopOpen (G) (x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land \exists v \in TopOpen (G) \exists t \in TopOpen (G) (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \to \exists v \in TopOpen (G) ((x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land \exists t \in TopOpen (G) (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u))$
32		simp31	$⊢ ((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \to x \in v$
33		elfpw	$⊢ y \in (𝒫 (A \times C) \cap Fin) \leftrightarrow (y \subseteq A \times C \land y \in Fin)$
34	33	simplbi	$⊢ y \in (𝒫 (A \times C) \cap Fin) \to y \subseteq A \times C$
35	34	ad2antrl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land (y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))) \to y \subseteq A \times C$
36		dmss	$⊢ y \subseteq A \times C \to dom y \subseteq dom (A \times C)$
37	35 36	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land (y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))) \to dom y \subseteq dom (A \times C)$
38		dmxpss	$⊢ dom (A \times C) \subseteq A$
39	37 38	sstrdi	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land (y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))) \to dom y \subseteq A$
40		elinel2	$⊢ y \in (𝒫 (A \times C) \cap Fin) \to y \in Fin$
41	40	ad2antrl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land (y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))) \to y \in Fin$
42		dmfi	$⊢ y \in Fin \to dom y \in Fin$
43	41 42	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land (y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))) \to dom y \in Fin$
44		elfpw	$⊢ dom y \in (𝒫 A \cap Fin) \leftrightarrow (dom y \subseteq A \land dom y \in Fin)$
45	39 43 44	sylanbrc	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land (y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))) \to dom y \in (𝒫 A \cap Fin)$
46		eqid	$⊢ \cdot_{G} = \cdot_{G}$
47		simpl11	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to φ$
48	47 2	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to G \in CMnd$
49	47 10	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to G \in TopMnd$
50		simprrl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to b \in (𝒫 A \cap Fin)$
51	50	elin2d	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to b \in Fin$
52		simpl2r	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to t \in TopOpen (G)$
53	49 20	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to G \in Mnd$
54	53 23	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to 0_{G} \in B$
55		hashcl	$⊢ b \in Fin \to \|b\| \in ℕ_{0}$
56	51 55	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to \|b\| \in ℕ_{0}$
57	1 46 22	mulgnn0z	$⊢ (G \in Mnd \land \|b\| \in ℕ_{0}) \to \|b\| \cdot_{G} 0_{G} = 0_{G}$
58	53 56 57	syl2anc	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to \|b\| \cdot_{G} 0_{G} = 0_{G}$
59		simpl32	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to 0_{G} \in t$
60	58 59	eqeltrd	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to \|b\| \cdot_{G} 0_{G} \in t$
61	13 1 46 48 49 51 52 54 60	tmdgsum2	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to \exists s \in TopOpen (G) (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)$
62		simp111	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to φ$
63	62 2	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to G \in CMnd$
64	62 3	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to G \in TopGrp$
65	62 4	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to A \in V$
66	62 5	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to C \in W$
67	62 6	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to F : A \times C ⟶ B$
68	62 7	syl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to H : A ⟶ B$
69	62 8	sylan	$⊢ ((((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \land j \in A) \to H (j) \in (G tsums (k \in C ⟼ j F k))$
70		eqid	$⊢ -_{G} = -_{G}$
71		simp3l	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to s \in TopOpen (G)$
72		simp3rl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to 0_{G} \in s$
73		simp2rl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to b \in (𝒫 A \cap Fin)$
74		simp2rr	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to dom y \subseteq b$
75		simp2ll	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to y \in (𝒫 (A \times C) \cap Fin)$
76	1 63 64 65 66 67 68 69 13 22 25 70 71 72 73 74 75	tsmsxplem1	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to \exists n \in (𝒫 C \cap Fin) (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)$
77	48	3adant3	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to G \in CMnd$
78	64	3adant3r	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to G \in TopGrp$
79	65	3adant3r	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to A \in V$
80	66	3adant3r	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to C \in W$
81	67	3adant3r	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to F : A \times C ⟶ B$
82	68	3adant3r	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to H : A ⟶ B$
83	47	3adant3	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to φ$
84	83 8	sylan	$⊢ ((((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \land j \in A) \to H (j) \in (G tsums (k \in C ⟼ j F k))$
85		simp3ll	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to s \in TopOpen (G)$
86	72	3adant3r	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to 0_{G} \in s$
87		simp2rl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to b \in (𝒫 A \cap Fin)$
88		simp133	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to \forall c \in v \forall d \in t c +_{G} d \in u$
89		simp3rl	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to n \in (𝒫 C \cap Fin)$
90		simp2ll	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to y \in (𝒫 (A \times C) \cap Fin)$
91		simp2rr	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to dom y \subseteq b$
92		simp3rr	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)$
93	92	simpld	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to ran y \subseteq n$
94		relxp	$⊢ Rel (A \times C)$
95		relss	$⊢ y \subseteq A \times C \to (Rel (A \times C) \to Rel y)$
96	34 94 95	mpisyl	$⊢ y \in (𝒫 (A \times C) \cap Fin) \to Rel y$
97		relssdmrn	$⊢ Rel y \to y \subseteq dom y \times ran y$
98	96 97	syl	$⊢ y \in (𝒫 (A \times C) \cap Fin) \to y \subseteq dom y \times ran y$
99		xpss12	$⊢ (dom y \subseteq b \land ran y \subseteq n) \to dom y \times ran y \subseteq b \times n$
100	98 99	sylan9ss	$⊢ (y \in (𝒫 (A \times C) \cap Fin) \land (dom y \subseteq b \land ran y \subseteq n)) \to y \subseteq b \times n$
101	90 91 93 100	syl12anc	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to y \subseteq b \times n$
102	92	simprd	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s$
103		sseq2	$⊢ z = b \times n \to (y \subseteq z \leftrightarrow y \subseteq b \times n)$
104		reseq2	$⊢ z = b \times n \to {F ↾}_{z} = {F ↾}_{(b \times n)}$
105	104	oveq2d	$⊢ z = b \times n \to \sum_{G} ({F ↾}_{z}) = \sum_{G} ({F ↾}_{(b \times n)})$
106	105	eleq1d	$⊢ z = b \times n \to (\sum_{G} ({F ↾}_{z}) \in v \leftrightarrow \sum_{G} ({F ↾}_{(b \times n)}) \in v)$
107	103 106	imbi12d	$⊢ z = b \times n \to ((y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v) \leftrightarrow (y \subseteq b \times n \to \sum_{G} ({F ↾}_{(b \times n)}) \in v))$
108		simp2lr	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)$
109		elfpw	$⊢ b \in (𝒫 A \cap Fin) \leftrightarrow (b \subseteq A \land b \in Fin)$
110		elfpw	$⊢ n \in (𝒫 C \cap Fin) \leftrightarrow (n \subseteq C \land n \in Fin)$
111		xpss12	$⊢ (b \subseteq A \land n \subseteq C) \to b \times n \subseteq A \times C$
112		xpfi	$⊢ (b \in Fin \land n \in Fin) \to b \times n \in Fin$
113	111 112	anim12i	$⊢ ((b \subseteq A \land n \subseteq C) \land (b \in Fin \land n \in Fin)) \to (b \times n \subseteq A \times C \land b \times n \in Fin)$
114	113	an4s	$⊢ ((b \subseteq A \land b \in Fin) \land (n \subseteq C \land n \in Fin)) \to (b \times n \subseteq A \times C \land b \times n \in Fin)$
115	109 110 114	syl2anb	$⊢ (b \in (𝒫 A \cap Fin) \land n \in (𝒫 C \cap Fin)) \to (b \times n \subseteq A \times C \land b \times n \in Fin)$
116		elfpw	$⊢ b \times n \in (𝒫 (A \times C) \cap Fin) \leftrightarrow (b \times n \subseteq A \times C \land b \times n \in Fin)$
117	115 116	sylibr	$⊢ (b \in (𝒫 A \cap Fin) \land n \in (𝒫 C \cap Fin)) \to b \times n \in (𝒫 (A \times C) \cap Fin)$
118	87 89 117	syl2anc	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to b \times n \in (𝒫 (A \times C) \cap Fin)$
119	107 108 118	rspcdva	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to (y \subseteq b \times n \to \sum_{G} ({F ↾}_{(b \times n)}) \in v)$
120	101 119	mpd	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to \sum_{G} ({F ↾}_{(b \times n)}) \in v$
121		simp3lr	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)$
122	121	simprd	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to \forall g \in (s^{b}) \sum_{G} g \in t$
123		oveq2	$⊢ g = h \to \sum_{G} g = \sum_{G} h$
124	123	eleq1d	$⊢ g = h \to (\sum_{G} g \in t \leftrightarrow \sum_{G} h \in t)$
125	124	cbvralvw	$⊢ \forall g \in (s^{b}) \sum_{G} g \in t \leftrightarrow \forall h \in (s^{b}) \sum_{G} h \in t$
126	122 125	sylib	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to \forall h \in (s^{b}) \sum_{G} h \in t$
127	1 77 78 79 80 81 82 84 13 22 25 70 85 86 87 88 89 101 102 120 126	tsmsxplem2	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)))) \to \sum_{G} ({H ↾}_{b}) \in u$
128	127	3exp	$⊢ ((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \to (((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \to (((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s))) \to \sum_{G} ({H ↾}_{b}) \in u))$
129	128	exp4a	$⊢ ((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \to (((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \to ((s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t)) \to ((n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s)) \to \sum_{G} ({H ↾}_{b}) \in u)))$
130	129	3imp1	$⊢ ((((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \land (n \in (𝒫 C \cap Fin) \land (ran y \subseteq n \land \forall x \in b H (x) -_{G} (\sum_{G}, ({F ↾}_{(\{x\} \times n)})) \in s))) \to \sum_{G} ({H ↾}_{b}) \in u$
131	76 130	rexlimddv	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to \sum_{G} ({H ↾}_{b}) \in u$
132	131	3expa	$⊢ ((((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \land (s \in TopOpen (G) \land (0_{G} \in s \land \forall g \in (s^{b}) \sum_{G} g \in t))) \to \sum_{G} ({H ↾}_{b}) \in u$
133	61 132	rexlimddv	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land ((y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b))) \to \sum_{G} ({H ↾}_{b}) \in u$
134	133	anassrs	$⊢ ((((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land (y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))) \land (b \in (𝒫 A \cap Fin) \land dom y \subseteq b)) \to \sum_{G} ({H ↾}_{b}) \in u$
135	134	expr	$⊢ ((((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land (y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))) \land b \in (𝒫 A \cap Fin)) \to (dom y \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u)$
136	135	ralrimiva	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land (y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))) \to \forall b \in (𝒫 A \cap Fin) (dom y \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u)$
137		sseq1	$⊢ a = dom y \to (a \subseteq b \leftrightarrow dom y \subseteq b)$
138	137	rspceaimv	$⊢ (dom y \in (𝒫 A \cap Fin) \land \forall b \in (𝒫 A \cap Fin) (dom y \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u)) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u)$
139	45 136 138	syl2anc	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \land (y \in (𝒫 (A \times C) \cap Fin) \land \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u)$
140	139	rexlimdvaa	$⊢ ((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \to (\exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u))$
141	32 140	embantd	$⊢ ((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G)) \land (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \to ((x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u))$
142	141	3expia	$⊢ ((φ \land u \in TopOpen (G) \land x \in u) \land (v \in TopOpen (G) \land t \in TopOpen (G))) \to ((x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u) \to ((x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u)))$
143	142	anassrs	$⊢ (((φ \land u \in TopOpen (G) \land x \in u) \land v \in TopOpen (G)) \land t \in TopOpen (G)) \to ((x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u) \to ((x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u)))$
144	143	rexlimdva	$⊢ ((φ \land u \in TopOpen (G) \land x \in u) \land v \in TopOpen (G)) \to (\exists t \in TopOpen (G) (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u) \to ((x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u)))$
145	144	impcomd	$⊢ ((φ \land u \in TopOpen (G) \land x \in u) \land v \in TopOpen (G)) \to (((x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land \exists t \in TopOpen (G) (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u))$
146	145	rexlimdva	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to (\exists v \in TopOpen (G) ((x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land \exists t \in TopOpen (G) (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u))$
147	31 146	syl5	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to ((\forall v \in TopOpen (G) (x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \land \exists v \in TopOpen (G) \exists t \in TopOpen (G) (x \in v \land 0_{G} \in t \land \forall c \in v \forall d \in t c +_{G} d \in u)) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u))$
148	30 147	mpan2d	$⊢ (φ \land u \in TopOpen (G) \land x \in u) \to (\forall v \in TopOpen (G) (x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u))$
149	148	3expia	$⊢ (φ \land u \in TopOpen (G)) \to (x \in u \to (\forall v \in TopOpen (G) (x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u)))$
150	149	com23	$⊢ (φ \land u \in TopOpen (G)) \to (\forall v \in TopOpen (G) (x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \to (x \in u \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u)))$
151	150	ralrimdva	$⊢ φ \to (\forall v \in TopOpen (G) (x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v)) \to \forall u \in TopOpen (G) (x \in u \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u)))$
152	151	anim2d	$⊢ φ \to ((x \in B \land \forall v \in TopOpen (G) (x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))) \to (x \in B \land \forall u \in TopOpen (G) (x \in u \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u))))$
153		eqid	$⊢ 𝒫 (A \times C) \cap Fin = 𝒫 (A \times C) \cap Fin$
154		tgptps	$⊢ G \in TopGrp \to G \in TopSp$
155	3 154	syl	$⊢ φ \to G \in TopSp$
156	4 5	xpexd	$⊢ φ \to A \times C \in V$
157	1 13 153 2 155 156 6	eltsms	$⊢ φ \to (x \in (G tsums F) \leftrightarrow (x \in B \land \forall v \in TopOpen (G) (x \in v \to \exists y \in (𝒫 (A \times C) \cap Fin) \forall z \in (𝒫 (A \times C) \cap Fin) (y \subseteq z \to \sum_{G} ({F ↾}_{z}) \in v))))$
158		eqid	$⊢ 𝒫 A \cap Fin = 𝒫 A \cap Fin$
159	1 13 158 2 155 4 7	eltsms	$⊢ φ \to (x \in (G tsums H) \leftrightarrow (x \in B \land \forall u \in TopOpen (G) (x \in u \to \exists a \in (𝒫 A \cap Fin) \forall b \in (𝒫 A \cap Fin) (a \subseteq b \to \sum_{G} ({H ↾}_{b}) \in u))))$
160	152 157 159	3imtr4d	$⊢ φ \to (x \in (G tsums F) \to x \in (G tsums H))$
161	160	ssrdv	$⊢ φ \to G tsums F \subseteq G tsums H$

Metamath Proof Explorer

Theorem tsmsxp

Proof