Theorem tmdgsum2 23447

Description: For any neighborhood 𝑈 of 𝑛𝑋, there is a neighborhood 𝑢 of 𝑋 such that any sum of 𝑛 elements in 𝑢 sums to an element of 𝑈. (Contributed by Mario Carneiro, 19-Sep-2015.)

Hypotheses

Ref	Expression
tmdgsum.j	⊢ 𝐽 = (TopOpen‘𝐺)
tmdgsum.b	⊢ 𝐵 = (Base‘𝐺)
tmdgsum2.t	⊢ · = (.g‘𝐺)
tmdgsum2.1	⊢ (𝜑 → 𝐺 ∈ CMnd)
tmdgsum2.2	⊢ (𝜑 → 𝐺 ∈ TopMnd)
tmdgsum2.a	⊢ (𝜑 → 𝐴 ∈ Fin)
tmdgsum2.u	⊢ (𝜑 → 𝑈 ∈ 𝐽)
tmdgsum2.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
tmdgsum2.3	⊢ (𝜑 → ((♯‘𝐴) · 𝑋) ∈ 𝑈)

Assertion

Ref	Expression
tmdgsum2	⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))

Distinct variable groups:   𝑢,𝑓,𝐴   𝑓,𝐽,𝑢   𝑓,𝑋,𝑢   𝐵,𝑓,𝑢   𝑓,𝐺,𝑢   𝑈,𝑓,𝑢

Allowed substitution hints:   𝜑(𝑢,𝑓)   · (𝑢,𝑓)

Proof of Theorem tmdgsum2

Dummy variables 𝑔 𝑘 𝑡 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2736	. . . . . . 7 ⊢ (𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) = (𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓))
2	1	mptpreima 6190	. . . . . 6 ⊢ (◡(𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}
3		tmdgsum2.1	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ CMnd)
4		tmdgsum2.2	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TopMnd)
5		tmdgsum2.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ Fin)
6		tmdgsum.j	. . . . . . . . 9 ⊢ 𝐽 = (TopOpen‘𝐺)
7		tmdgsum.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐺)
8	6, 7	tmdgsum 23446	. . . . . . . 8 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽))
9	3, 4, 5, 8	syl3anc 1371	. . . . . . 7 ⊢ (𝜑 → (𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽))
10		tmdgsum2.u	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ 𝐽)
11		cnima 22616	. . . . . . 7 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽) ∧ 𝑈 ∈ 𝐽) → (◡(𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) ∈ (𝐽 ↑ko 𝒫 𝐴))
12	9, 10, 11	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (◡(𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) ∈ (𝐽 ↑ko 𝒫 𝐴))
13	2, 12	eqeltrrid 2843	. . . . 5 ⊢ (𝜑 → {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (𝐽 ↑ko 𝒫 𝐴))
14	6, 7	tmdtopon 23432	. . . . . . . 8 ⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵))
15		topontop 22262	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
16	4, 14, 15	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
17		xkopt 23006	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin) → (𝐽 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝐽})))
18	16, 5, 17	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐽 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝐽})))
19		fnconstg 6730	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝐵) → (𝐴 × {𝐽}) Fn 𝐴)
20	4, 14, 19	3syl 18	. . . . . . 7 ⊢ (𝜑 → (𝐴 × {𝐽}) Fn 𝐴)
21		eqid 2736	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}
22	21	ptval 22921	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ (𝐴 × {𝐽}) Fn 𝐴) → (∏t‘(𝐴 × {𝐽})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
23	5, 20, 22	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (∏t‘(𝐴 × {𝐽})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
24	18, 23	eqtrd 2776	. . . . 5 ⊢ (𝜑 → (𝐽 ↑ko 𝒫 𝐴) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
25	13, 24	eleqtrd 2840	. . . 4 ⊢ (𝜑 → {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
26		oveq2 7365	. . . . . 6 ⊢ (𝑓 = (𝐴 × {𝑋}) → (𝐺 Σg 𝑓) = (𝐺 Σg (𝐴 × {𝑋})))
27	26	eleq1d 2822	. . . . 5 ⊢ (𝑓 = (𝐴 × {𝑋}) → ((𝐺 Σg 𝑓) ∈ 𝑈 ↔ (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈))
28		tmdgsum2.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
29		fconst6g 6731	. . . . . . 7 ⊢ (𝑋 ∈ 𝐵 → (𝐴 × {𝑋}):𝐴⟶𝐵)
30	28, 29	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐴 × {𝑋}):𝐴⟶𝐵)
31	7	fvexi 6856	. . . . . . 7 ⊢ 𝐵 ∈ V
32		elmapg 8778	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ Fin) → ((𝐴 × {𝑋}) ∈ (𝐵 ↑m 𝐴) ↔ (𝐴 × {𝑋}):𝐴⟶𝐵))
33	31, 5, 32	sylancr 587	. . . . . 6 ⊢ (𝜑 → ((𝐴 × {𝑋}) ∈ (𝐵 ↑m 𝐴) ↔ (𝐴 × {𝑋}):𝐴⟶𝐵))
34	30, 33	mpbird 256	. . . . 5 ⊢ (𝜑 → (𝐴 × {𝑋}) ∈ (𝐵 ↑m 𝐴))
35		fconstmpt 5694	. . . . . . . 8 ⊢ (𝐴 × {𝑋}) = (𝑘 ∈ 𝐴 ↦ 𝑋)
36	35	oveq2i 7368	. . . . . . 7 ⊢ (𝐺 Σg (𝐴 × {𝑋})) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋))
37		cmnmnd 19579	. . . . . . . . 9 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
38	3, 37	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ Mnd)
39		tmdgsum2.t	. . . . . . . . 9 ⊢ · = (.g‘𝐺)
40	7, 39	gsumconst 19711	. . . . . . . 8 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((♯‘𝐴) · 𝑋))
41	38, 5, 28, 40	syl3anc 1371	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((♯‘𝐴) · 𝑋))
42	36, 41	eqtrid 2788	. . . . . 6 ⊢ (𝜑 → (𝐺 Σg (𝐴 × {𝑋})) = ((♯‘𝐴) · 𝑋))
43		tmdgsum2.3	. . . . . 6 ⊢ (𝜑 → ((♯‘𝐴) · 𝑋) ∈ 𝑈)
44	42, 43	eqeltrd 2838	. . . . 5 ⊢ (𝜑 → (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈)
45	27, 34, 44	elrabd 3647	. . . 4 ⊢ (𝜑 → (𝐴 × {𝑋}) ∈ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})
46		tg2 22315	. . . 4 ⊢ (({𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}) ∧ (𝐴 × {𝑋}) ∈ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
47	25, 45, 46	syl2anc 584	. . 3 ⊢ (𝜑 → ∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
48		eleq2 2826	. . . . 5 ⊢ (𝑡 = 𝑥 → ((𝐴 × {𝑋}) ∈ 𝑡 ↔ (𝐴 × {𝑋}) ∈ 𝑥))
49		sseq1 3969	. . . . 5 ⊢ (𝑡 = 𝑥 → (𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
50	48, 49	anbi12d 631	. . . 4 ⊢ (𝑡 = 𝑥 → (((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
51	50	rexab2 3657	. . 3 ⊢ (∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
52	47, 51	sylib 217	. 2 ⊢ (𝜑 → ∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
53		toponuni 22263	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
54	4, 14, 53	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 = ∪ 𝐽)
55	54	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐵 = ∪ 𝐽)
56	55	ineq1d 4171	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐵 ∩ ∩ ran 𝑔) = (∪ 𝐽 ∩ ∩ ran 𝑔))
57	16	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐽 ∈ Top)
58		simplrl 775	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔 Fn 𝐴)
59		simplrr 776	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))
60		fvconst2g 7151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝐽})‘𝑦) = 𝐽)
61	60	eleq2d 2823	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐴) → ((𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ (𝑔‘𝑦) ∈ 𝐽))
62	61	ralbidva 3172	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽))
63	57, 62	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽))
64	59, 63	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽)
65		ffnfv 7066	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝐴⟶𝐽 ↔ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽))
66	58, 64, 65	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔:𝐴⟶𝐽)
67	66	frnd 6676	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ran 𝑔 ⊆ 𝐽)
68	5	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐴 ∈ Fin)
69		dffn4 6762	. . . . . . . . . . . . . 14 ⊢ (𝑔 Fn 𝐴 ↔ 𝑔:𝐴–onto→ran 𝑔)
70	58, 69	sylib 217	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔:𝐴–onto→ran 𝑔)
71		fofi 9282	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑔:𝐴–onto→ran 𝑔) → ran 𝑔 ∈ Fin)
72	68, 70, 71	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ran 𝑔 ∈ Fin)
73		eqid 2736	. . . . . . . . . . . . 13 ⊢ ∪ 𝐽 = ∪ 𝐽
74	73	rintopn 22258	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ran 𝑔 ⊆ 𝐽 ∧ ran 𝑔 ∈ Fin) → (∪ 𝐽 ∩ ∩ ran 𝑔) ∈ 𝐽)
75	57, 67, 72, 74	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∪ 𝐽 ∩ ∩ ran 𝑔) ∈ 𝐽)
76	56, 75	eqeltrd 2838	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐵 ∩ ∩ ran 𝑔) ∈ 𝐽)
77	28	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑋 ∈ 𝐵)
78		fconstmpt 5694	. . . . . . . . . . . . . 14 ⊢ (𝐴 × {𝑋}) = (𝑦 ∈ 𝐴 ↦ 𝑋)
79		simprl 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
80	78, 79	eqeltrrid 2843	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
81		mptelixpg 8873	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Fin → ((𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
82	68, 81	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ((𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
83	80, 82	mpbid 231	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦))
84		eleq2 2826	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑔‘𝑦) → (𝑋 ∈ 𝑧 ↔ 𝑋 ∈ (𝑔‘𝑦)))
85	84	ralrn 7038	. . . . . . . . . . . . 13 ⊢ (𝑔 Fn 𝐴 → (∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
86	58, 85	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
87	83, 86	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧)
88		elrint 4952	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔) ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧))
89	77, 87, 88	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔))
90	31	inex1 5274	. . . . . . . . . . . . 13 ⊢ (𝐵 ∩ ∩ ran 𝑔) ∈ V
91		ixpconstg 8844	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∩ ∩ ran 𝑔) ∈ V) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) = ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴))
92	68, 90, 91	sylancl 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) = ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴))
93		inss2 4189	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∩ ∩ ran 𝑔) ⊆ ∩ ran 𝑔
94		fnfvelrn 7031	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) ∈ ran 𝑔)
95		intss1 4924	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔‘𝑦) ∈ ran 𝑔 → ∩ ran 𝑔 ⊆ (𝑔‘𝑦))
96	94, 95	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → ∩ ran 𝑔 ⊆ (𝑔‘𝑦))
97	93, 96	sstrid 3955	. . . . . . . . . . . . . 14 ⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐵 ∩ ∩ ran 𝑔) ⊆ (𝑔‘𝑦))
98	97	ralrimiva 3143	. . . . . . . . . . . . 13 ⊢ (𝑔 Fn 𝐴 → ∀𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ (𝑔‘𝑦))
99		ss2ixp 8848	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ (𝑔‘𝑦) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
100	58, 98, 99	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
101	92, 100	eqsstrrd 3983	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴) ⊆ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
102		ssrab 4030	. . . . . . . . . . . . 13 ⊢ (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ (𝐵 ↑m 𝐴) ∧ ∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈))
103	102	simprbi 497	. . . . . . . . . . . 12 ⊢ (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} → ∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈)
104	103	ad2antll 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈)
105		ssralv 4010	. . . . . . . . . . 11 ⊢ (((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴) ⊆ X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈 → ∀𝑓 ∈ ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
106	101, 104, 105	sylc 65	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑓 ∈ ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)
107		eleq2 2826	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐵 ∩ ∩ ran 𝑔) → (𝑋 ∈ 𝑢 ↔ 𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔)))
108		oveq1 7364	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝐵 ∩ ∩ ran 𝑔) → (𝑢 ↑m 𝐴) = ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴))
109	108	raleqdv 3313	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐵 ∩ ∩ ran 𝑔) → (∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈 ↔ ∀𝑓 ∈ ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
110	107, 109	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑢 = (𝐵 ∩ ∩ ran 𝑔) → ((𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈) ↔ (𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔) ∧ ∀𝑓 ∈ ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
111	110	rspcev 3581	. . . . . . . . . 10 ⊢ (((𝐵 ∩ ∩ ran 𝑔) ∈ 𝐽 ∧ (𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔) ∧ ∀𝑓 ∈ ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
112	76, 89, 106, 111	syl12anc 835	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
113	112	ex 413	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) → (((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
114	113	3adantr3 1171	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦))) → (((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
115		eleq2 2826	. . . . . . . . 9 ⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → ((𝐴 × {𝑋}) ∈ 𝑥 ↔ (𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦)))
116		sseq1 3969	. . . . . . . . 9 ⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
117	115, 116	anbi12d 631	. . . . . . . 8 ⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
118	117	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → ((((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) ↔ (((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
119	114, 118	syl5ibrcom 246	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦))) → (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
120	119	expimpd 454	. . . . 5 ⊢ (𝜑 → (((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
121	120	exlimdv 1936	. . . 4 ⊢ (𝜑 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
122	121	impd 411	. . 3 ⊢ (𝜑 → ((∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
123	122	exlimdv 1936	. 2 ⊢ (𝜑 → (∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
124	52, 123	mpd 15	1 ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2713  ∀wral 3064  ∃wrex 3073  {crab 3407  Vcvv 3445   ∖ cdif 3907   ∩ cin 3909   ⊆ wss 3910  𝒫 cpw 4560  {csn 4586  ∪ cuni 4865  ∩ cint 4907   ↦ cmpt 5188   × cxp 5631  ^◡ccnv 5632  ran crn 5634   “ cima 5636   Fn wfn 6491  ⟶wf 6492  –onto→wfo 6494  ‘cfv 6496  (class class class)co 7357   ↑_m cmap 8765  Xcixp 8835  Fincfn 8883  ♯chash 14230  Basecbs 17083  TopOpenctopn 17303  topGenctg 17319  ∏_tcpt 17320   Σ_g cgsu 17322  Mndcmnd 18556  ._gcmg 18872  CMndccmn 19562  Topctop 22242  TopOnctopon 22259   Cn ccn 22575   ↑_ko cxko 22912  TopMndctmd 23421

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-seq 13907  df-hash 14231  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-rest 17304  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-mre 17466  df-mrc 17467  df-acs 17469  df-plusf 18496  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cn 22578  df-cnp 22579  df-cmp 22738  df-tx 22913  df-xko 22914  df-tmd 23423

This theorem is referenced by:  tsmsxp  23506