Theorem tmdgsum2 22859

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 2739	. . . . . . 7 ⊢ (𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) = (𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓))
2	1	mptpreima 6080	. . . . . 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 22858	. . . . . . . 8 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽))
9	3, 4, 5, 8	syl3anc 1372	. . . . . . 7 ⊢ (𝜑 → (𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽))
10		tmdgsum2.u	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ 𝐽)
11		cnima 22028	. . . . . . 7 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽) ∧ 𝑈 ∈ 𝐽) → (◡(𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) ∈ (𝐽 ↑ko 𝒫 𝐴))
12	9, 10, 11	syl2anc 587	. . . . . 6 ⊢ (𝜑 → (◡(𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) ∈ (𝐽 ↑ko 𝒫 𝐴))
13	2, 12	eqeltrrid 2839	. . . . 5 ⊢ (𝜑 → {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (𝐽 ↑ko 𝒫 𝐴))
14	6, 7	tmdtopon 22844	. . . . . . . 8 ⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵))
15		topontop 21676	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
16	4, 14, 15	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
17		xkopt 22418	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin) → (𝐽 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝐽})))
18	16, 5, 17	syl2anc 587	. . . . . 6 ⊢ (𝜑 → (𝐽 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝐽})))
19		fnconstg 6576	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝐵) → (𝐴 × {𝐽}) Fn 𝐴)
20	4, 14, 19	3syl 18	. . . . . . 7 ⊢ (𝜑 → (𝐴 × {𝐽}) Fn 𝐴)
21		eqid 2739	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}
22	21	ptval 22333	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ (𝐴 × {𝐽}) Fn 𝐴) → (∏t‘(𝐴 × {𝐽})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
23	5, 20, 22	syl2anc 587	. . . . . 6 ⊢ (𝜑 → (∏t‘(𝐴 × {𝐽})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
24	18, 23	eqtrd 2774	. . . . 5 ⊢ (𝜑 → (𝐽 ↑ko 𝒫 𝐴) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
25	13, 24	eleqtrd 2836	. . . 4 ⊢ (𝜑 → {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
26		oveq2 7190	. . . . . 6 ⊢ (𝑓 = (𝐴 × {𝑋}) → (𝐺 Σg 𝑓) = (𝐺 Σg (𝐴 × {𝑋})))
27	26	eleq1d 2818	. . . . 5 ⊢ (𝑓 = (𝐴 × {𝑋}) → ((𝐺 Σg 𝑓) ∈ 𝑈 ↔ (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈))
28		tmdgsum2.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
29		fconst6g 6577	. . . . . . 7 ⊢ (𝑋 ∈ 𝐵 → (𝐴 × {𝑋}):𝐴⟶𝐵)
30	28, 29	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐴 × {𝑋}):𝐴⟶𝐵)
31	7	fvexi 6700	. . . . . . 7 ⊢ 𝐵 ∈ V
32		elmapg 8462	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ Fin) → ((𝐴 × {𝑋}) ∈ (𝐵 ↑m 𝐴) ↔ (𝐴 × {𝑋}):𝐴⟶𝐵))
33	31, 5, 32	sylancr 590	. . . . . 6 ⊢ (𝜑 → ((𝐴 × {𝑋}) ∈ (𝐵 ↑m 𝐴) ↔ (𝐴 × {𝑋}):𝐴⟶𝐵))
34	30, 33	mpbird 260	. . . . 5 ⊢ (𝜑 → (𝐴 × {𝑋}) ∈ (𝐵 ↑m 𝐴))
35		fconstmpt 5595	. . . . . . . 8 ⊢ (𝐴 × {𝑋}) = (𝑘 ∈ 𝐴 ↦ 𝑋)
36	35	oveq2i 7193	. . . . . . 7 ⊢ (𝐺 Σg (𝐴 × {𝑋})) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋))
37		cmnmnd 19052	. . . . . . . . 9 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
38	3, 37	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ Mnd)
39		tmdgsum2.t	. . . . . . . . 9 ⊢ · = (.g‘𝐺)
40	7, 39	gsumconst 19185	. . . . . . . 8 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((♯‘𝐴) · 𝑋))
41	38, 5, 28, 40	syl3anc 1372	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((♯‘𝐴) · 𝑋))
42	36, 41	syl5eq 2786	. . . . . 6 ⊢ (𝜑 → (𝐺 Σg (𝐴 × {𝑋})) = ((♯‘𝐴) · 𝑋))
43		tmdgsum2.3	. . . . . 6 ⊢ (𝜑 → ((♯‘𝐴) · 𝑋) ∈ 𝑈)
44	42, 43	eqeltrd 2834	. . . . 5 ⊢ (𝜑 → (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈)
45	27, 34, 44	elrabd 3595	. . . 4 ⊢ (𝜑 → (𝐴 × {𝑋}) ∈ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})
46		tg2 21728	. . . 4 ⊢ (({𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}) ∧ (𝐴 × {𝑋}) ∈ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
47	25, 45, 46	syl2anc 587	. . 3 ⊢ (𝜑 → ∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
48		eleq2 2822	. . . . 5 ⊢ (𝑡 = 𝑥 → ((𝐴 × {𝑋}) ∈ 𝑡 ↔ (𝐴 × {𝑋}) ∈ 𝑥))
49		sseq1 3912	. . . . 5 ⊢ (𝑡 = 𝑥 → (𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
50	48, 49	anbi12d 634	. . . 4 ⊢ (𝑡 = 𝑥 → (((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
51	50	rexab2 3604	. . 3 ⊢ (∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
52	47, 51	sylib 221	. 2 ⊢ (𝜑 → ∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
53		toponuni 21677	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
54	4, 14, 53	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 = ∪ 𝐽)
55	54	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐵 = ∪ 𝐽)
56	55	ineq1d 4112	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐵 ∩ ∩ ran 𝑔) = (∪ 𝐽 ∩ ∩ ran 𝑔))
57	16	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐽 ∈ Top)
58		simplrl 777	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔 Fn 𝐴)
59		simplrr 778	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))
60		fvconst2g 6986	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝐽})‘𝑦) = 𝐽)
61	60	eleq2d 2819	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐴) → ((𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ (𝑔‘𝑦) ∈ 𝐽))
62	61	ralbidva 3109	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽))
63	57, 62	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽))
64	59, 63	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽)
65		ffnfv 6904	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝐴⟶𝐽 ↔ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽))
66	58, 64, 65	sylanbrc 586	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔:𝐴⟶𝐽)
67	66	frnd 6522	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ran 𝑔 ⊆ 𝐽)
68	5	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐴 ∈ Fin)
69		dffn4 6608	. . . . . . . . . . . . . 14 ⊢ (𝑔 Fn 𝐴 ↔ 𝑔:𝐴–onto→ran 𝑔)
70	58, 69	sylib 221	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔:𝐴–onto→ran 𝑔)
71		fofi 8895	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑔:𝐴–onto→ran 𝑔) → ran 𝑔 ∈ Fin)
72	68, 70, 71	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ran 𝑔 ∈ Fin)
73		eqid 2739	. . . . . . . . . . . . 13 ⊢ ∪ 𝐽 = ∪ 𝐽
74	73	rintopn 21672	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ran 𝑔 ⊆ 𝐽 ∧ ran 𝑔 ∈ Fin) → (∪ 𝐽 ∩ ∩ ran 𝑔) ∈ 𝐽)
75	57, 67, 72, 74	syl3anc 1372	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∪ 𝐽 ∩ ∩ ran 𝑔) ∈ 𝐽)
76	56, 75	eqeltrd 2834	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐵 ∩ ∩ ran 𝑔) ∈ 𝐽)
77	28	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑋 ∈ 𝐵)
78		fconstmpt 5595	. . . . . . . . . . . . . 14 ⊢ (𝐴 × {𝑋}) = (𝑦 ∈ 𝐴 ↦ 𝑋)
79		simprl 771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
80	78, 79	eqeltrrid 2839	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
81		mptelixpg 8557	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Fin → ((𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
82	68, 81	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ((𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
83	80, 82	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦))
84		eleq2 2822	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑔‘𝑦) → (𝑋 ∈ 𝑧 ↔ 𝑋 ∈ (𝑔‘𝑦)))
85	84	ralrn 6876	. . . . . . . . . . . . 13 ⊢ (𝑔 Fn 𝐴 → (∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
86	58, 85	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
87	83, 86	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧)
88		elrint 4889	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔) ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧))
89	77, 87, 88	sylanbrc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔))
90	31	inex1 5195	. . . . . . . . . . . . 13 ⊢ (𝐵 ∩ ∩ ran 𝑔) ∈ V
91		ixpconstg 8528	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∩ ∩ ran 𝑔) ∈ V) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) = ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴))
92	68, 90, 91	sylancl 589	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) = ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴))
93		inss2 4130	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∩ ∩ ran 𝑔) ⊆ ∩ ran 𝑔
94		fnfvelrn 6870	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) ∈ ran 𝑔)
95		intss1 4861	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔‘𝑦) ∈ ran 𝑔 → ∩ ran 𝑔 ⊆ (𝑔‘𝑦))
96	94, 95	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → ∩ ran 𝑔 ⊆ (𝑔‘𝑦))
97	93, 96	sstrid 3898	. . . . . . . . . . . . . 14 ⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐵 ∩ ∩ ran 𝑔) ⊆ (𝑔‘𝑦))
98	97	ralrimiva 3097	. . . . . . . . . . . . 13 ⊢ (𝑔 Fn 𝐴 → ∀𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ (𝑔‘𝑦))
99		ss2ixp 8532	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ (𝑔‘𝑦) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
100	58, 98, 99	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
101	92, 100	eqsstrrd 3926	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴) ⊆ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
102		ssrab 3972	. . . . . . . . . . . . 13 ⊢ (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ (𝐵 ↑m 𝐴) ∧ ∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈))
103	102	simprbi 500	. . . . . . . . . . . 12 ⊢ (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} → ∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈)
104	103	ad2antll 729	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈)
105		ssralv 3953	. . . . . . . . . . 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 2822	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐵 ∩ ∩ ran 𝑔) → (𝑋 ∈ 𝑢 ↔ 𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔)))
108		oveq1 7189	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝐵 ∩ ∩ ran 𝑔) → (𝑢 ↑m 𝐴) = ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴))
109	108	raleqdv 3317	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐵 ∩ ∩ ran 𝑔) → (∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈 ↔ ∀𝑓 ∈ ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
110	107, 109	anbi12d 634	. . . . . . . . . . 11 ⊢ (𝑢 = (𝐵 ∩ ∩ ran 𝑔) → ((𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈) ↔ (𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔) ∧ ∀𝑓 ∈ ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
111	110	rspcev 3529	. . . . . . . . . 10 ⊢ (((𝐵 ∩ ∩ ran 𝑔) ∈ 𝐽 ∧ (𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔) ∧ ∀𝑓 ∈ ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
112	76, 89, 106, 111	syl12anc 836	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
113	112	ex 416	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) → (((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
114	113	3adantr3 1172	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦))) → (((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
115		eleq2 2822	. . . . . . . . 9 ⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → ((𝐴 × {𝑋}) ∈ 𝑥 ↔ (𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦)))
116		sseq1 3912	. . . . . . . . 9 ⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
117	115, 116	anbi12d 634	. . . . . . . 8 ⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
118	117	imbi1d 345	. . . . . . 7 ⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → ((((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) ↔ (((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
119	114, 118	syl5ibrcom 250	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦))) → (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
120	119	expimpd 457	. . . . 5 ⊢ (𝜑 → (((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
121	120	exlimdv 1940	. . . 4 ⊢ (𝜑 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
122	121	impd 414	. . 3 ⊢ (𝜑 → ((∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
123	122	exlimdv 1940	. 2 ⊢ (𝜑 → (∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
124	52, 123	mpd 15	1 ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1088   = wceq 1542  ∃wex 1786   ∈ wcel 2114  {cab 2717  ∀wral 3054  ∃wrex 3055  {crab 3058  Vcvv 3400   ∖ cdif 3850   ∩ cin 3852   ⊆ wss 3853  𝒫 cpw 4498  {csn 4526  ∪ cuni 4806  ∩ cint 4846   ↦ cmpt 5120   × cxp 5533  ^◡ccnv 5534  ran crn 5536   “ cima 5538   Fn wfn 6344  ⟶wf 6345  –onto→wfo 6347  ‘cfv 6349  (class class class)co 7182   ↑_m cmap 8449  Xcixp 8519  Fincfn 8567  ♯chash 13794  Basecbs 16598  TopOpenctopn 16810  topGenctg 16826  ∏_tcpt 16827   Σ_g cgsu 16829  Mndcmnd 18039  ._gcmg 18354  CMndccmn 19036  Topctop 21656  TopOnctopon 21673   Cn ccn 21987   ↑_ko cxko 22324  TopMndctmd 22833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5242  ax-pr 5306  ax-un 7491  ax-cnex 10683  ax-resscn 10684  ax-1cn 10685  ax-icn 10686  ax-addcl 10687  ax-addrcl 10688  ax-mulcl 10689  ax-mulrcl 10690  ax-mulcom 10691  ax-addass 10692  ax-mulass 10693  ax-distr 10694  ax-i2m1 10695  ax-1ne0 10696  ax-1rid 10697  ax-rnegex 10698  ax-rrecex 10699  ax-cnre 10700  ax-pre-lttri 10701  ax-pre-lttrn 10702  ax-pre-ltadd 10703  ax-pre-mulgt0 10704

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3402  df-sbc 3686  df-csb 3801  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4222  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4807  df-int 4847  df-iun 4893  df-iin 4894  df-br 5041  df-opab 5103  df-mpt 5121  df-tr 5147  df-id 5439  df-eprel 5444  df-po 5452  df-so 5453  df-fr 5493  df-se 5494  df-we 5495  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-rn 5546  df-res 5547  df-ima 5548  df-pred 6139  df-ord 6185  df-on 6186  df-lim 6187  df-suc 6188  df-iota 6307  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7139  df-ov 7185  df-oprab 7186  df-mpo 7187  df-of 7437  df-om 7612  df-1st 7726  df-2nd 7727  df-supp 7869  df-wrecs 7988  df-recs 8049  df-rdg 8087  df-1o 8143  df-er 8332  df-map 8451  df-ixp 8520  df-en 8568  df-dom 8569  df-sdom 8570  df-fin 8571  df-fsupp 8919  df-fi 8960  df-oi 9059  df-card 9453  df-pnf 10767  df-mnf 10768  df-xr 10769  df-ltxr 10770  df-le 10771  df-sub 10962  df-neg 10963  df-nn 11729  df-2 11791  df-n0 11989  df-z 12075  df-uz 12337  df-fz 12994  df-fzo 13137  df-seq 13473  df-hash 13795  df-ndx 16601  df-slot 16602  df-base 16604  df-sets 16605  df-ress 16606  df-plusg 16693  df-rest 16811  df-0g 16830  df-gsum 16831  df-topgen 16832  df-pt 16833  df-mre 16972  df-mrc 16973  df-acs 16975  df-plusf 17979  df-mgm 17980  df-sgrp 18029  df-mnd 18040  df-submnd 18085  df-mulg 18355  df-cntz 18577  df-cmn 19038  df-top 21657  df-topon 21674  df-topsp 21696  df-bases 21709  df-cn 21990  df-cnp 21991  df-cmp 22150  df-tx 22325  df-xko 22326  df-tmd 22835

This theorem is referenced by:  tsmsxp  22918