tmdgsum2

Description: For any neighborhood U of n X , there is a neighborhood u of X such that any sum of n elements in u sums to an element of U . (Contributed by Mario Carneiro, 19-Sep-2015)

	Ref	Expression
Hypotheses	tmdgsum.j	$⊢ J = TopOpen (G)$
	tmdgsum.b	$⊢ B = {Base}_{G}$
	tmdgsum2.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	tmdgsum2.1	$⊢ φ \to G \in CMnd$
	tmdgsum2.2	$⊢ φ \to G \in TopMnd$
	tmdgsum2.a	$⊢ φ \to A \in Fin$
	tmdgsum2.u	$⊢ φ \to U \in J$
	tmdgsum2.x	$⊢ φ \to X \in B$
	tmdgsum2.3	$⊢ φ \to \|A\| \underset{˙}{\cdot} X \in U$
Assertion	tmdgsum2	$⊢ φ \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U)$

Proof

Step	Hyp	Ref	Expression
1		tmdgsum.j	$⊢ J = TopOpen (G)$
2		tmdgsum.b	$⊢ B = {Base}_{G}$
3		tmdgsum2.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		tmdgsum2.1	$⊢ φ \to G \in CMnd$
5		tmdgsum2.2	$⊢ φ \to G \in TopMnd$
6		tmdgsum2.a	$⊢ φ \to A \in Fin$
7		tmdgsum2.u	$⊢ φ \to U \in J$
8		tmdgsum2.x	$⊢ φ \to X \in B$
9		tmdgsum2.3	$⊢ φ \to \|A\| \underset{˙}{\cdot} X \in U$
10		eqid	$⊢ (f \in (B^{A}) ⟼ \sum_{G} f) = (f \in (B^{A}) ⟼ \sum_{G} f)$
11	10	mptpreima	$⊢ {(f \in (B^{A}) ⟼ \sum_{G} f)}^{-1} [U] = \{f \in (B^{A}) \| \sum_{G} f \in U\}$
12	1 2	tmdgsum	$⊢ (G \in CMnd \land G \in TopMnd \land A \in Fin) \to (f \in (B^{A}) ⟼ \sum_{G} f) \in ((J^_{ko} 𝒫 A) Cn J)$
13	4 5 6 12	syl3anc	$⊢ φ \to (f \in (B^{A}) ⟼ \sum_{G} f) \in ((J^_{ko} 𝒫 A) Cn J)$
14		cnima	$⊢ ((f \in (B^{A}) ⟼ \sum_{G} f) \in ((J^_{ko} 𝒫 A) Cn J) \land U \in J) \to {(f \in (B^{A}) ⟼ \sum_{G} f)}^{-1} [U] \in (J^_{ko} 𝒫 A)$
15	13 7 14	syl2anc	$⊢ φ \to {(f \in (B^{A}) ⟼ \sum_{G} f)}^{-1} [U] \in (J^_{ko} 𝒫 A)$
16	11 15	eqeltrrid	$⊢ φ \to \{f \in (B^{A}) \| \sum_{G} f \in U\} \in (J^_{ko} 𝒫 A)$
17	1 2	tmdtopon	$⊢ G \in TopMnd \to J \in TopOn (B)$
18		topontop	$⊢ J \in TopOn (B) \to J \in Top$
19	5 17 18	3syl	$⊢ φ \to J \in Top$
20		xkopt	$⊢ (J \in Top \land A \in Fin) \to J^_{ko} 𝒫 A = \prod_{𝑡} (A \times \{J\})$
21	19 6 20	syl2anc	$⊢ φ \to J^_{ko} 𝒫 A = \prod_{𝑡} (A \times \{J\})$
22		fnconstg	$⊢ J \in TopOn (B) \to (A \times \{J\}) Fn A$
23	5 17 22	3syl	$⊢ φ \to (A \times \{J\}) Fn A$
24		eqid	$⊢ \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y))\} = \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y))\}$
25	24	ptval	$⊢ (A \in Fin \land (A \times \{J\}) Fn A) \to \prod_{𝑡} (A \times \{J\}) = topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
26	6 23 25	syl2anc	$⊢ φ \to \prod_{𝑡} (A \times \{J\}) = topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
27	21 26	eqtrd	$⊢ φ \to J^_{ko} 𝒫 A = topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
28	16 27	eleqtrd	$⊢ φ \to \{f \in (B^{A}) \| \sum_{G} f \in U\} \in topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
29		oveq2	$⊢ f = A \times \{X\} \to \sum_{G} f = \sum_{G} (A \times \{X\})$
30	29	eleq1d	$⊢ f = A \times \{X\} \to (\sum_{G} f \in U \leftrightarrow \sum_{G} (A \times \{X\}) \in U)$
31		fconst6g	$⊢ X \in B \to (A \times \{X\}) : A ⟶ B$
32	8 31	syl	$⊢ φ \to (A \times \{X\}) : A ⟶ B$
33	2	fvexi	$⊢ B \in V$
34		elmapg	$⊢ (B \in V \land A \in Fin) \to (A \times \{X\} \in (B^{A}) \leftrightarrow (A \times \{X\}) : A ⟶ B)$
35	33 6 34	sylancr	$⊢ φ \to (A \times \{X\} \in (B^{A}) \leftrightarrow (A \times \{X\}) : A ⟶ B)$
36	32 35	mpbird	$⊢ φ \to A \times \{X\} \in (B^{A})$
37		fconstmpt	$⊢ A \times \{X\} = (k \in A ⟼ X)$
38	37	oveq2i	$⊢ \sum_{G} (A \times \{X\}) = \underset{k \in A}{\sum_{G}} X$
39		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
40	4 39	syl	$⊢ φ \to G \in Mnd$
41	2 3	gsumconst	$⊢ (G \in Mnd \land A \in Fin \land X \in B) \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X$
42	40 6 8 41	syl3anc	$⊢ φ \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X$
43	38 42	eqtrid	$⊢ φ \to \sum_{G} (A \times \{X\}) = \|A\| \underset{˙}{\cdot} X$
44	43 9	eqeltrd	$⊢ φ \to \sum_{G} (A \times \{X\}) \in U$
45	30 36 44	elrabd	$⊢ φ \to A \times \{X\} \in \{f \in (B^{A}) \| \sum_{G} f \in U\}$
46		tg2	$⊢ (\{f \in (B^{A}) \| \sum_{G} f \in U\} \in topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y))\}) \land A \times \{X\} \in \{f \in (B^{A}) \| \sum_{G} f \in U\}) \to \exists t \in \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y))\} (A \times \{X\} \in t \land t \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})$
47	28 45 46	syl2anc	$⊢ φ \to \exists t \in \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y))\} (A \times \{X\} \in t \land t \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})$
48		eleq2	$⊢ t = x \to (A \times \{X\} \in t \leftrightarrow A \times \{X\} \in x)$
49		sseq1	$⊢ t = x \to (t \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\} \leftrightarrow x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})$
50	48 49	anbi12d	$⊢ t = x \to ((A \times \{X\} \in t \land t \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}) \leftrightarrow (A \times \{X\} \in x \land x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}))$
51	50	rexab2	$⊢ \exists t \in \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y))\} (A \times \{X\} \in t \land t \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}) \leftrightarrow \exists x (\exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y)) \land (A \times \{X\} \in x \land x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}))$
52	47 51	sylib	$⊢ φ \to \exists x (\exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y)) \land (A \times \{X\} \in x \land x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}))$
53		toponuni	$⊢ J \in TopOn (B) \to B = ⋃ J$
54	5 17 53	3syl	$⊢ φ \to B = ⋃ J$
55	54	ad2antrr	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to B = ⋃ J$
56	55	ineq1d	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to B \cap ⋂ ran g = ⋃ J \cap ⋂ ran g$
57	19	ad2antrr	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to J \in Top$
58		simplrl	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to g Fn A$
59		simplrr	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to \forall y \in A g (y) \in (A \times \{J\}) (y)$
60		fvconst2g	$⊢ (J \in Top \land y \in A) \to (A \times \{J\}) (y) = J$
61	60	eleq2d	$⊢ (J \in Top \land y \in A) \to (g (y) \in (A \times \{J\}) (y) \leftrightarrow g (y) \in J)$
62	61	ralbidva	$⊢ J \in Top \to (\forall y \in A g (y) \in (A \times \{J\}) (y) \leftrightarrow \forall y \in A g (y) \in J)$
63	57 62	syl	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to (\forall y \in A g (y) \in (A \times \{J\}) (y) \leftrightarrow \forall y \in A g (y) \in J)$
64	59 63	mpbid	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to \forall y \in A g (y) \in J$
65		ffnfv	$⊢ g : A ⟶ J \leftrightarrow (g Fn A \land \forall y \in A g (y) \in J)$
66	58 64 65	sylanbrc	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to g : A ⟶ J$
67	66	frnd	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to ran g \subseteq J$
68	6	ad2antrr	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to A \in Fin$
69		dffn4	$⊢ g Fn A \leftrightarrow g : A \underset{onto}{⟶} ran g$
70	58 69	sylib	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to g : A \underset{onto}{⟶} ran g$
71		fofi	$⊢ (A \in Fin \land g : A \underset{onto}{⟶} ran g) \to ran g \in Fin$
72	68 70 71	syl2anc	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to ran g \in Fin$
73		eqid	$⊢ ⋃ J = ⋃ J$
74	73	rintopn	$⊢ (J \in Top \land ran g \subseteq J \land ran g \in Fin) \to ⋃ J \cap ⋂ ran g \in J$
75	57 67 72 74	syl3anc	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to ⋃ J \cap ⋂ ran g \in J$
76	56 75	eqeltrd	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to B \cap ⋂ ran g \in J$
77	8	ad2antrr	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to X \in B$
78		fconstmpt	$⊢ A \times \{X\} = (y \in A ⟼ X)$
79		simprl	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to A \times \{X\} \in \underset{y \in A}{⨉} g (y)$
80	78 79	eqeltrrid	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to (y \in A ⟼ X) \in \underset{y \in A}{⨉} g (y)$
81		mptelixpg	$⊢ A \in Fin \to ((y \in A ⟼ X) \in \underset{y \in A}{⨉} g (y) \leftrightarrow \forall y \in A X \in g (y))$
82	68 81	syl	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to ((y \in A ⟼ X) \in \underset{y \in A}{⨉} g (y) \leftrightarrow \forall y \in A X \in g (y))$
83	80 82	mpbid	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to \forall y \in A X \in g (y)$
84		eleq2	$⊢ z = g (y) \to (X \in z \leftrightarrow X \in g (y))$
85	84	ralrn	$⊢ g Fn A \to (\forall z \in ran g X \in z \leftrightarrow \forall y \in A X \in g (y))$
86	58 85	syl	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to (\forall z \in ran g X \in z \leftrightarrow \forall y \in A X \in g (y))$
87	83 86	mpbird	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to \forall z \in ran g X \in z$
88		elrint	$⊢ X \in (B \cap ⋂ ran g) \leftrightarrow (X \in B \land \forall z \in ran g X \in z)$
89	77 87 88	sylanbrc	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to X \in (B \cap ⋂ ran g)$
90	33	inex1	$⊢ B \cap ⋂ ran g \in V$
91		ixpconstg	$⊢ (A \in Fin \land B \cap ⋂ ran g \in V) \to \underset{y \in A}{⨉} (B \cap ⋂ ran g) = {(B \cap ⋂ ran g)}^{A}$
92	68 90 91	sylancl	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to \underset{y \in A}{⨉} (B \cap ⋂ ran g) = {(B \cap ⋂ ran g)}^{A}$
93		inss2	$⊢ B \cap ⋂ ran g \subseteq ⋂ ran g$
94		fnfvelrn	$⊢ (g Fn A \land y \in A) \to g (y) \in ran g$
95		intss1	$⊢ g (y) \in ran g \to ⋂ ran g \subseteq g (y)$
96	94 95	syl	$⊢ (g Fn A \land y \in A) \to ⋂ ran g \subseteq g (y)$
97	93 96	sstrid	$⊢ (g Fn A \land y \in A) \to B \cap ⋂ ran g \subseteq g (y)$
98	97	ralrimiva	$⊢ g Fn A \to \forall y \in A B \cap ⋂ ran g \subseteq g (y)$
99		ss2ixp	$⊢ \forall y \in A B \cap ⋂ ran g \subseteq g (y) \to \underset{y \in A}{⨉} (B \cap ⋂ ran g) \subseteq \underset{y \in A}{⨉} g (y)$
100	58 98 99	3syl	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to \underset{y \in A}{⨉} (B \cap ⋂ ran g) \subseteq \underset{y \in A}{⨉} g (y)$
101	92 100	eqsstrrd	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to {(B \cap ⋂ ran g)}^{A} \subseteq \underset{y \in A}{⨉} g (y)$
102		ssrab	$⊢ \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\} \leftrightarrow (\underset{y \in A}{⨉} g (y) \subseteq B^{A} \land \forall f \in \underset{y \in A}{⨉} g (y) \sum_{G} f \in U)$
103	102	simprbi	$⊢ \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\} \to \forall f \in \underset{y \in A}{⨉} g (y) \sum_{G} f \in U$
104	103	ad2antll	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to \forall f \in \underset{y \in A}{⨉} g (y) \sum_{G} f \in U$
105		ssralv	$⊢ {(B \cap ⋂ ran g)}^{A} \subseteq \underset{y \in A}{⨉} g (y) \to (\forall f \in \underset{y \in A}{⨉} g (y) \sum_{G} f \in U \to \forall f \in ({(B \cap ⋂ ran g)}^{A}) \sum_{G} f \in U)$
106	101 104 105	sylc	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to \forall f \in ({(B \cap ⋂ ran g)}^{A}) \sum_{G} f \in U$
107		eleq2	$⊢ u = B \cap ⋂ ran g \to (X \in u \leftrightarrow X \in (B \cap ⋂ ran g))$
108		oveq1	$⊢ u = B \cap ⋂ ran g \to u^{A} = {(B \cap ⋂ ran g)}^{A}$
109	108	raleqdv	$⊢ u = B \cap ⋂ ran g \to (\forall f \in (u^{A}) \sum_{G} f \in U \leftrightarrow \forall f \in ({(B \cap ⋂ ran g)}^{A}) \sum_{G} f \in U)$
110	107 109	anbi12d	$⊢ u = B \cap ⋂ ran g \to ((X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U) \leftrightarrow (X \in (B \cap ⋂ ran g) \land \forall f \in ({(B \cap ⋂ ran g)}^{A}) \sum_{G} f \in U))$
111	110	rspcev	$⊢ (B \cap ⋂ ran g \in J \land (X \in (B \cap ⋂ ran g) \land \forall f \in ({(B \cap ⋂ ran g)}^{A}) \sum_{G} f \in U)) \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U)$
112	76 89 106 111	syl12anc	$⊢ ((φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \land (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U)$
113	112	ex	$⊢ (φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y))) \to ((A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}) \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U))$
114	113	3adantr3	$⊢ (φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y))) \to ((A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}) \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U))$
115		eleq2	$⊢ x = \underset{y \in A}{⨉} g (y) \to (A \times \{X\} \in x \leftrightarrow A \times \{X\} \in \underset{y \in A}{⨉} g (y))$
116		sseq1	$⊢ x = \underset{y \in A}{⨉} g (y) \to (x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\} \leftrightarrow \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})$
117	115 116	anbi12d	$⊢ x = \underset{y \in A}{⨉} g (y) \to ((A \times \{X\} \in x \land x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}) \leftrightarrow (A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}))$
118	117	imbi1d	$⊢ x = \underset{y \in A}{⨉} g (y) \to (((A \times \{X\} \in x \land x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}) \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U)) \leftrightarrow ((A \times \{X\} \in \underset{y \in A}{⨉} g (y) \land \underset{y \in A}{⨉} g (y) \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}) \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U)))$
119	114 118	syl5ibrcom	$⊢ (φ \land (g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y))) \to (x = \underset{y \in A}{⨉} g (y) \to ((A \times \{X\} \in x \land x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}) \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U)))$
120	119	expimpd	$⊢ φ \to (((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y)) \to ((A \times \{X\} \in x \land x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}) \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U)))$
121	120	exlimdv	$⊢ φ \to (\exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y)) \to ((A \times \{X\} \in x \land x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\}) \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U)))$
122	121	impd	$⊢ φ \to ((\exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y)) \land (A \times \{X\} \in x \land x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U))$
123	122	exlimdv	$⊢ φ \to (\exists x (\exists g ((g Fn A \land \forall y \in A g (y) \in (A \times \{J\}) (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ (A \times \{J\}) (y)) \land x = \underset{y \in A}{⨉} g (y)) \land (A \times \{X\} \in x \land x \subseteq \{f \in (B^{A}) \| \sum_{G} f \in U\})) \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U))$
124	52 123	mpd	$⊢ φ \to \exists u \in J (X \in u \land \forall f \in (u^{A}) \sum_{G} f \in U)$

Metamath Proof Explorer

Theorem tmdgsum2

Proof