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	$⊢ B = {Base}_{G}$
	eltsms.j	$⊢ J = TopOpen (G)$
	eltsms.s	$⊢ S = 𝒫 A \cap Fin$
	eltsms.1	$⊢ φ \to G \in CMnd$
	eltsms.2	$⊢ φ \to G \in TopSp$
	eltsms.a	$⊢ φ \to A \in V$
	eltsms.f	$⊢ φ \to F : A ⟶ B$
	tsmsi.3	$⊢ φ \to C \in (G tsums F)$
	tsmsi.4	$⊢ φ \to U \in J$
	tsmsi.5	$⊢ φ \to C \in U$
Assertion	tsmsi	$⊢ φ \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in U)$

Proof

Step	Hyp	Ref	Expression
1		eltsms.b	$⊢ B = {Base}_{G}$
2		eltsms.j	$⊢ J = TopOpen (G)$
3		eltsms.s	$⊢ S = 𝒫 A \cap Fin$
4		eltsms.1	$⊢ φ \to G \in CMnd$
5		eltsms.2	$⊢ φ \to G \in TopSp$
6		eltsms.a	$⊢ φ \to A \in V$
7		eltsms.f	$⊢ φ \to F : A ⟶ B$
8		tsmsi.3	$⊢ φ \to C \in (G tsums F)$
9		tsmsi.4	$⊢ φ \to U \in J$
10		tsmsi.5	$⊢ φ \to C \in U$
11		eleq2	$⊢ u = U \to (C \in u \leftrightarrow C \in U)$
12		eleq2	$⊢ u = U \to (\sum_{G} ({F ↾}_{y}) \in u \leftrightarrow \sum_{G} ({F ↾}_{y}) \in U)$
13	12	imbi2d	$⊢ u = U \to ((z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u) \leftrightarrow (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in U))$
14	13	rexralbidv	$⊢ u = U \to (\exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u) \leftrightarrow \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in U))$
15	11 14	imbi12d	$⊢ u = U \to ((C \in u \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)) \leftrightarrow (C \in U \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in U)))$
16	1 2 3 4 5 6 7	eltsms	$⊢ φ \to (C \in (G tsums F) \leftrightarrow (C \in B \land \forall u \in J (C \in u \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))))$
17	8 16	mpbid	$⊢ φ \to (C \in B \land \forall u \in J (C \in u \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)))$
18	17	simprd	$⊢ φ \to \forall u \in J (C \in u \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))$
19	15 18 9	rspcdva	$⊢ φ \to (C \in U \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in U))$
20	10 19	mpd	$⊢ φ \to \exists z \in S \forall y \in S (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in U)$

Metamath Proof Explorer

Theorem tsmsi

Proof