tsmscls

Description: One half of tgptsmscls , true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015)

	Ref	Expression
Hypotheses	tsmscls.b	$⊢ B = {Base}_{G}$
	tsmscls.j	$⊢ J = TopOpen (G)$
	tsmscls.1	$⊢ φ \to G \in CMnd$
	tsmscls.2	$⊢ φ \to G \in TopSp$
	tsmscls.a	$⊢ φ \to A \in V$
	tsmscls.f	$⊢ φ \to F : A ⟶ B$
	tsmscls.x	$⊢ φ \to X \in (G tsums F)$
Assertion	tsmscls	$⊢ φ \to cls (J) (\{X\}) \subseteq G tsums F$

Proof

Step	Hyp	Ref	Expression
1		tsmscls.b	$⊢ B = {Base}_{G}$
2		tsmscls.j	$⊢ J = TopOpen (G)$
3		tsmscls.1	$⊢ φ \to G \in CMnd$
4		tsmscls.2	$⊢ φ \to G \in TopSp$
5		tsmscls.a	$⊢ φ \to A \in V$
6		tsmscls.f	$⊢ φ \to F : A ⟶ B$
7		tsmscls.x	$⊢ φ \to X \in (G tsums F)$
8		eqid	$⊢ 𝒫 A \cap Fin = 𝒫 A \cap Fin$
9		eqid	$⊢ ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}) = ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\})$
10	1 2 8 9 4 5 6	tsmsval	$⊢ φ \to G tsums F = (J fLimf ((𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}))) ((y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y})))$
11	1 2	istps	$⊢ G \in TopSp \leftrightarrow J \in TopOn (B)$
12	4 11	sylib	$⊢ φ \to J \in TopOn (B)$
13		eqid	$⊢ (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}) = (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\})$
14	8 13 9 5	tsmsfbas	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}) \in fBas (𝒫 A \cap Fin)$
15		fgcl	$⊢ ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}) \in fBas (𝒫 A \cap Fin) \to (𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}) \in Fil (𝒫 A \cap Fin)$
16	14 15	syl	$⊢ φ \to (𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}) \in Fil (𝒫 A \cap Fin)$
17	1 8 3 5 6	tsmslem1	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{G} ({F ↾}_{y}) \in B$
18	17	fmpttd	$⊢ φ \to (y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y})) : 𝒫 A \cap Fin ⟶ B$
19		flfval	$⊢ (J \in TopOn (B) \land (𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}) \in Fil (𝒫 A \cap Fin) \land (y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y})) : 𝒫 A \cap Fin ⟶ B) \to (J fLimf ((𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}))) ((y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y}))) = J fLim (B FilMap (y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y}))) ((𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}))$
20	12 16 18 19	syl3anc	$⊢ φ \to (J fLimf ((𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}))) ((y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y}))) = J fLim (B FilMap (y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y}))) ((𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}))$
21	10 20	eqtrd	$⊢ φ \to G tsums F = J fLim (B FilMap (y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y}))) ((𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}))$
22	7 21	eleqtrd	$⊢ φ \to X \in (J fLim (B FilMap (y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y}))) ((𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\})))$
23		flimsncls	$⊢ X \in (J fLim (B FilMap (y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y}))) ((𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}))) \to cls (J) (\{X\}) \subseteq J fLim (B FilMap (y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y}))) ((𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}))$
24	22 23	syl	$⊢ φ \to cls (J) (\{X\}) \subseteq J fLim (B FilMap (y \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{y}))) ((𝒫 A \cap Fin) filGen ran (x \in (𝒫 A \cap Fin) ⟼ \{y \in (𝒫 A \cap Fin) \| x \subseteq y\}))$
25	24 21	sseqtrrd	$⊢ φ \to cls (J) (\{X\}) \subseteq G tsums F$

Metamath Proof Explorer

Theorem tsmscls

Proof