Theorem tmdgsum2 24051

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 2734	. . . . . . 7 ⊢ (𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) = (𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓))
2	1	mptpreima 6238	. . . . . 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 24050	. . . . . . . 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 23220	. . . . . . 7 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽) ∧ 𝑈 ∈ 𝐽) → (◡(𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) ∈ (𝐽 ↑ko 𝒫 𝐴))
12	9, 10, 11	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (◡(𝑓 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) ∈ (𝐽 ↑ko 𝒫 𝐴))
13	2, 12	eqeltrrid 2838	. . . . 5 ⊢ (𝜑 → {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (𝐽 ↑ko 𝒫 𝐴))
14	6, 7	tmdtopon 24036	. . . . . . . 8 ⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵))
15		topontop 22868	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
16	4, 14, 15	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
17		xkopt 23610	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin) → (𝐽 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝐽})))
18	16, 5, 17	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐽 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝐽})))
19		fnconstg 6776	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝐵) → (𝐴 × {𝐽}) Fn 𝐴)
20	4, 14, 19	3syl 18	. . . . . . 7 ⊢ (𝜑 → (𝐴 × {𝐽}) Fn 𝐴)
21		eqid 2734	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}
22	21	ptval 23525	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ (𝐴 × {𝐽}) Fn 𝐴) → (∏t‘(𝐴 × {𝐽})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
23	5, 20, 22	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (∏t‘(𝐴 × {𝐽})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
24	18, 23	eqtrd 2769	. . . . 5 ⊢ (𝜑 → (𝐽 ↑ko 𝒫 𝐴) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
25	13, 24	eleqtrd 2835	. . . 4 ⊢ (𝜑 → {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}))
26		oveq2 7421	. . . . . 6 ⊢ (𝑓 = (𝐴 × {𝑋}) → (𝐺 Σg 𝑓) = (𝐺 Σg (𝐴 × {𝑋})))
27	26	eleq1d 2818	. . . . 5 ⊢ (𝑓 = (𝐴 × {𝑋}) → ((𝐺 Σg 𝑓) ∈ 𝑈 ↔ (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈))
28		tmdgsum2.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
29		fconst6g 6777	. . . . . . 7 ⊢ (𝑋 ∈ 𝐵 → (𝐴 × {𝑋}):𝐴⟶𝐵)
30	28, 29	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐴 × {𝑋}):𝐴⟶𝐵)
31	7	fvexi 6900	. . . . . . 7 ⊢ 𝐵 ∈ V
32		elmapg 8861	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ Fin) → ((𝐴 × {𝑋}) ∈ (𝐵 ↑m 𝐴) ↔ (𝐴 × {𝑋}):𝐴⟶𝐵))
33	31, 5, 32	sylancr 587	. . . . . 6 ⊢ (𝜑 → ((𝐴 × {𝑋}) ∈ (𝐵 ↑m 𝐴) ↔ (𝐴 × {𝑋}):𝐴⟶𝐵))
34	30, 33	mpbird 257	. . . . 5 ⊢ (𝜑 → (𝐴 × {𝑋}) ∈ (𝐵 ↑m 𝐴))
35		fconstmpt 5727	. . . . . . . 8 ⊢ (𝐴 × {𝑋}) = (𝑘 ∈ 𝐴 ↦ 𝑋)
36	35	oveq2i 7424	. . . . . . 7 ⊢ (𝐺 Σg (𝐴 × {𝑋})) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋))
37		cmnmnd 19784	. . . . . . . . 9 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
38	3, 37	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ Mnd)
39		tmdgsum2.t	. . . . . . . . 9 ⊢ · = (.g‘𝐺)
40	7, 39	gsumconst 19921	. . . . . . . 8 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((♯‘𝐴) · 𝑋))
41	38, 5, 28, 40	syl3anc 1372	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((♯‘𝐴) · 𝑋))
42	36, 41	eqtrid 2781	. . . . . 6 ⊢ (𝜑 → (𝐺 Σg (𝐴 × {𝑋})) = ((♯‘𝐴) · 𝑋))
43		tmdgsum2.3	. . . . . 6 ⊢ (𝜑 → ((♯‘𝐴) · 𝑋) ∈ 𝑈)
44	42, 43	eqeltrd 2833	. . . . 5 ⊢ (𝜑 → (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈)
45	27, 34, 44	elrabd 3677	. . . 4 ⊢ (𝜑 → (𝐴 × {𝑋}) ∈ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})
46		tg2 22920	. . . 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 2822	. . . . 5 ⊢ (𝑡 = 𝑥 → ((𝐴 × {𝑋}) ∈ 𝑡 ↔ (𝐴 × {𝑋}) ∈ 𝑥))
49		sseq1 3989	. . . . 5 ⊢ (𝑡 = 𝑥 → (𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
50	48, 49	anbi12d 632	. . . 4 ⊢ (𝑡 = 𝑥 → (((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
51	50	rexab2 3687	. . 3 ⊢ (∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
52	47, 51	sylib 218	. 2 ⊢ (𝜑 → ∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
53		toponuni 22869	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
54	4, 14, 53	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 = ∪ 𝐽)
55	54	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐵 = ∪ 𝐽)
56	55	ineq1d 4199	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐵 ∩ ∩ ran 𝑔) = (∪ 𝐽 ∩ ∩ ran 𝑔))
57	16	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐽 ∈ Top)
58		simplrl 776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔 Fn 𝐴)
59		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))
60		fvconst2g 7204	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝐽})‘𝑦) = 𝐽)
61	60	eleq2d 2819	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐴) → ((𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ (𝑔‘𝑦) ∈ 𝐽))
62	61	ralbidva 3163	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽))
63	57, 62	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽))
64	59, 63	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽)
65		ffnfv 7119	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝐴⟶𝐽 ↔ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽))
66	58, 64, 65	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔:𝐴⟶𝐽)
67	66	frnd 6724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ran 𝑔 ⊆ 𝐽)
68	5	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐴 ∈ Fin)
69		dffn4 6806	. . . . . . . . . . . . . 14 ⊢ (𝑔 Fn 𝐴 ↔ 𝑔:𝐴–onto→ran 𝑔)
70	58, 69	sylib 218	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔:𝐴–onto→ran 𝑔)
71		fofi 9333	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑔:𝐴–onto→ran 𝑔) → ran 𝑔 ∈ Fin)
72	68, 70, 71	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ran 𝑔 ∈ Fin)
73		eqid 2734	. . . . . . . . . . . . 13 ⊢ ∪ 𝐽 = ∪ 𝐽
74	73	rintopn 22864	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ran 𝑔 ⊆ 𝐽 ∧ ran 𝑔 ∈ Fin) → (∪ 𝐽 ∩ ∩ ran 𝑔) ∈ 𝐽)
75	57, 67, 72, 74	syl3anc 1372	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∪ 𝐽 ∩ ∩ ran 𝑔) ∈ 𝐽)
76	56, 75	eqeltrd 2833	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐵 ∩ ∩ ran 𝑔) ∈ 𝐽)
77	28	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑋 ∈ 𝐵)
78		fconstmpt 5727	. . . . . . . . . . . . . 14 ⊢ (𝐴 × {𝑋}) = (𝑦 ∈ 𝐴 ↦ 𝑋)
79		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
80	78, 79	eqeltrrid 2838	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
81		mptelixpg 8957	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Fin → ((𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
82	68, 81	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ((𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
83	80, 82	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦))
84		eleq2 2822	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑔‘𝑦) → (𝑋 ∈ 𝑧 ↔ 𝑋 ∈ (𝑔‘𝑦)))
85	84	ralrn 7088	. . . . . . . . . . . . 13 ⊢ (𝑔 Fn 𝐴 → (∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
86	58, 85	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)))
87	83, 86	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧)
88		elrint 4969	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔) ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧))
89	77, 87, 88	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔))
90	31	inex1 5297	. . . . . . . . . . . . 13 ⊢ (𝐵 ∩ ∩ ran 𝑔) ∈ V
91		ixpconstg 8928	. . . . . . . . . . . . 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 4218	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∩ ∩ ran 𝑔) ⊆ ∩ ran 𝑔
94		fnfvelrn 7080	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) ∈ ran 𝑔)
95		intss1 4943	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔‘𝑦) ∈ ran 𝑔 → ∩ ran 𝑔 ⊆ (𝑔‘𝑦))
96	94, 95	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → ∩ ran 𝑔 ⊆ (𝑔‘𝑦))
97	93, 96	sstrid 3975	. . . . . . . . . . . . . 14 ⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐵 ∩ ∩ ran 𝑔) ⊆ (𝑔‘𝑦))
98	97	ralrimiva 3133	. . . . . . . . . . . . 13 ⊢ (𝑔 Fn 𝐴 → ∀𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ (𝑔‘𝑦))
99		ss2ixp 8932	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ (𝑔‘𝑦) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
100	58, 98, 99	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran 𝑔) ⊆ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
101	92, 100	eqsstrrd 3999	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴) ⊆ X𝑦 ∈ 𝐴 (𝑔‘𝑦))
102		ssrab 4053	. . . . . . . . . . . . 13 ⊢ (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ (𝐵 ↑m 𝐴) ∧ ∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈))
103	102	simprbi 496	. . . . . . . . . . . 12 ⊢ (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} → ∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈)
104	103	ad2antll 729	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈)
105		ssralv 4032	. . . . . . . . . . 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 7420	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝐵 ∩ ∩ ran 𝑔) → (𝑢 ↑m 𝐴) = ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴))
109	108	raleqdv 3309	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐵 ∩ ∩ ran 𝑔) → (∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈 ↔ ∀𝑓 ∈ ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
110	107, 109	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑢 = (𝐵 ∩ ∩ ran 𝑔) → ((𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈) ↔ (𝑋 ∈ (𝐵 ∩ ∩ ran 𝑔) ∧ ∀𝑓 ∈ ((𝐵 ∩ ∩ ran 𝑔) ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
111	110	rspcev 3605	. . . . . . . . . 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 412	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) → (((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
114	113	3adantr3 1171	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦))) → (((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
115		eleq2 2822	. . . . . . . . 9 ⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → ((𝐴 × {𝑋}) ∈ 𝑥 ↔ (𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦)))
116		sseq1 3989	. . . . . . . . 9 ⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
117	115, 116	anbi12d 632	. . . . . . . 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 247	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦))) → (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
120	119	expimpd 453	. . . . 5 ⊢ (𝜑 → (((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
121	120	exlimdv 1932	. . . 4 ⊢ (𝜑 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
122	121	impd 410	. . 3 ⊢ (𝜑 → ((∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
123	122	exlimdv 1932	. 2 ⊢ (𝜑 → (∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
124	52, 123	mpd 15	1 ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539  ∃wex 1778   ∈ wcel 2107  {cab 2712  ∀wral 3050  ∃wrex 3059  {crab 3419  Vcvv 3463   ∖ cdif 3928   ∩ cin 3930   ⊆ wss 3931  𝒫 cpw 4580  {csn 4606  ∪ cuni 4887  ∩ cint 4926   ↦ cmpt 5205   × cxp 5663  ^◡ccnv 5664  ran crn 5666   “ cima 5668   Fn wfn 6536  ⟶wf 6537  –onto→wfo 6539  ‘cfv 6541  (class class class)co 7413   ↑_m cmap 8848  Xcixp 8919  Fincfn 8967  ♯chash 14352  Basecbs 17230  TopOpenctopn 17438  topGenctg 17454  ∏_tcpt 17455   Σ_g cgsu 17457  Mndcmnd 18717  ._gcmg 19055  CMndccmn 19767  Topctop 22848  TopOnctopon 22865   Cn ccn 23179   ↑_ko cxko 23516  TopMndctmd 24025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-cnex 11193  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-int 4927  df-iun 4973  df-iin 4974  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-se 5618  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-om 7870  df-1st 7996  df-2nd 7997  df-supp 8168  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-er 8727  df-map 8850  df-ixp 8920  df-en 8968  df-dom 8969  df-sdom 8970  df-fin 8971  df-fsupp 9384  df-fi 9433  df-oi 9532  df-card 9961  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477  df-nn 12249  df-2 12311  df-n0 12510  df-z 12597  df-uz 12861  df-fz 13530  df-fzo 13677  df-seq 14025  df-hash 14353  df-sets 17184  df-slot 17202  df-ndx 17214  df-base 17231  df-ress 17254  df-plusg 17287  df-rest 17439  df-0g 17458  df-gsum 17459  df-topgen 17460  df-pt 17461  df-mre 17601  df-mrc 17602  df-acs 17604  df-plusf 18622  df-mgm 18623  df-sgrp 18702  df-mnd 18718  df-submnd 18767  df-mulg 19056  df-cntz 19305  df-cmn 19769  df-top 22849  df-topon 22866  df-topsp 22888  df-bases 22901  df-cn 23182  df-cnp 23183  df-cmp 23342  df-tx 23517  df-xko 23518  df-tmd 24027

This theorem is referenced by:  tsmsxp  24110