Theorem ptcnp 22232

Description: If every projection of a function is continuous at 𝐷, then the function itself is continuous at 𝐷 into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)

Hypotheses

Ref	Expression
ptcnp.2	⊢ 𝐾 = (∏t‘𝐹)
ptcnp.3	⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
ptcnp.4	⊢ (𝜑 → 𝐼 ∈ 𝑉)
ptcnp.5	⊢ (𝜑 → 𝐹:𝐼⟶Top)
ptcnp.6	⊢ (𝜑 → 𝐷 ∈ 𝑋)
ptcnp.7	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))

Assertion

Ref	Expression
ptcnp	⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝐷))

Distinct variable groups:   𝑥,𝑘,𝐷   𝑘,𝐼,𝑥   𝑘,𝐽   𝜑,𝑘,𝑥   𝑘,𝐹,𝑥   𝑘,𝑉,𝑥   𝑘,𝑋,𝑥

Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐽(𝑥)   𝐾(𝑥,𝑘)

Proof of Theorem ptcnp

Dummy variables 𝑓 𝑔 𝑤 𝑧 𝑎 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptcnp.3	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
2	1	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐽 ∈ (TopOn‘𝑋))
3		ptcnp.5	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐼⟶Top)
4	3	ffvelrnda 6853	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ Top)
5		toptopon2 21528	. . . . . . . . 9 ⊢ ((𝐹‘𝑘) ∈ Top ↔ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
6	4, 5	sylib 220	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
7		ptcnp.7	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))
8		cnpf2 21860	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)) ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
9	2, 6, 7, 8	syl3anc 1367	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ (𝐹‘𝑘))
10	9	fvmptelrn 6879	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ∪ (𝐹‘𝑘))
11	10	an32s 650	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → 𝐴 ∈ ∪ (𝐹‘𝑘))
12	11	ralrimiva 3184	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑘 ∈ 𝐼 𝐴 ∈ ∪ (𝐹‘𝑘))
13		ptcnp.4	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
14	13	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐼 ∈ 𝑉)
15		mptelixpg 8501	. . . . 5 ⊢ (𝐼 ∈ 𝑉 → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ ∪ (𝐹‘𝑘)))
16	14, 15	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘) ↔ ∀𝑘 ∈ 𝐼 𝐴 ∈ ∪ (𝐹‘𝑘)))
17	12, 16	mpbird 259	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ 𝐼 ↦ 𝐴) ∈ X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘))
18	17	fmpttd 6881	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)):𝑋⟶X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘))
19		df-3an 1085	. . . . . . . 8 ⊢ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)))
20		ptcnp.2	. . . . . . . . . . . . 13 ⊢ 𝐾 = (∏t‘𝐹)
21		ptcnp.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ 𝑋)
22		nfv 1915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛))
23		nfv 1915	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))
24		nfcv 2979	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘𝑋
25		nfmpt1 5166	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘(𝑘 ∈ 𝐼 ↦ 𝐴)
26	24, 25	nfmpt 5165	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))
27		nfcv 2979	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘𝐷
28	26, 27	nffv 6682	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷)
29	28	nfel1 2996	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)
30	23, 29	nfan 1900	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛))
31	22, 30	nfan 1900	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))
32		simprll 777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → 𝑔 Fn 𝐼)
33		simprlr 778	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛))
34		fveq2 6672	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → (𝑔‘𝑛) = (𝑔‘𝑘))
35		fveq2 6672	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
36	34, 35	eleq12d 2909	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝑔‘𝑘) ∈ (𝐹‘𝑘)))
37	36	rspccva 3624	. . . . . . . . . . . . . 14 ⊢ ((∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ 𝑘 ∈ 𝐼) → (𝑔‘𝑘) ∈ (𝐹‘𝑘))
38	33, 37	sylan 582	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) ∧ 𝑘 ∈ 𝐼) → (𝑔‘𝑘) ∈ (𝐹‘𝑘))
39		simprrl 779	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → (𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)))
40	39	simpld 497	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → 𝑤 ∈ Fin)
41	39	simprd 498	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))
42	35	unieqd 4854	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑘))
43	34, 42	eqeq12d 2839	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝑔‘𝑛) = ∪ (𝐹‘𝑛) ↔ (𝑔‘𝑘) = ∪ (𝐹‘𝑘)))
44	43	rspccva 3624	. . . . . . . . . . . . . 14 ⊢ ((∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛) ∧ 𝑘 ∈ (𝐼 ∖ 𝑤)) → (𝑔‘𝑘) = ∪ (𝐹‘𝑘))
45	41, 44	sylan 582	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) ∧ 𝑘 ∈ (𝐼 ∖ 𝑤)) → (𝑔‘𝑘) = ∪ (𝐹‘𝑘))
46		simprrr 780	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛))
47	34	cbvixpv 8481	. . . . . . . . . . . . . 14 ⊢ X𝑛 ∈ 𝐼 (𝑔‘𝑛) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)
48	46, 47	eleqtrdi 2925	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝑔‘𝑘))
49	20, 1, 13, 3, 21, 7, 31, 32, 38, 40, 45, 48	ptcnplem 22231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
50	49	anassrs 470	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛))) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛))) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
51	50	expr 459	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛))) ∧ (𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
52	51	rexlimdvaa 3287	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛))) → (∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
53	52	impr 457	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
54	19, 53	sylan2b 595	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
55		eleq2 2903	. . . . . . . 8 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛)))
56	47	eqeq2i 2836	. . . . . . . . . . . 12 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) ↔ 𝑓 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))
57	56	biimpi 218	. . . . . . . . . . 11 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → 𝑓 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))
58	57	sseq2d 4001	. . . . . . . . . 10 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓 ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘)))
59	58	anbi2d 630	. . . . . . . . 9 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ((𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓) ↔ (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
60	59	rexbidv 3299	. . . . . . . 8 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → (∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓) ↔ ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘))))
61	55, 60	imbi12d 347	. . . . . . 7 ⊢ (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ((((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓)) ↔ (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑛 ∈ 𝐼 (𝑔‘𝑛) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝑔‘𝑘)))))
62	54, 61	syl5ibrcom 249	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛))) → (𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓))))
63	62	expimpd 456	. . . . 5 ⊢ (𝜑 → (((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓))))
64	63	exlimdv 1934	. . . 4 ⊢ (𝜑 → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓))))
65	64	alrimiv 1928	. . 3 ⊢ (𝜑 → ∀𝑓(∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓))))
66		eqeq1 2827	. . . . . 6 ⊢ (𝑎 = 𝑓 → (𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛) ↔ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)))
67	66	anbi2d 630	. . . . 5 ⊢ (𝑎 = 𝑓 → (((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))))
68	67	exbidv 1922	. . . 4 ⊢ (𝑎 = 𝑓 → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))))
69	68	ralab 3686	. . 3 ⊢ (∀𝑓 ∈ {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))} (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓)) ↔ ∀𝑓(∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (𝑔‘𝑛)) → (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓))))
70	65, 69	sylibr 236	. 2 ⊢ (𝜑 → ∀𝑓 ∈ {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))} (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓)))
71	3	ffnd 6517	. . . . 5 ⊢ (𝜑 → 𝐹 Fn 𝐼)
72		eqid 2823	. . . . . 6 ⊢ {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))} = {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))}
73	72	ptval 22180	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 Fn 𝐼) → (∏t‘𝐹) = (topGen‘{𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))}))
74	13, 71, 73	syl2anc 586	. . . 4 ⊢ (𝜑 → (∏t‘𝐹) = (topGen‘{𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))}))
75	20, 74	syl5eq 2870	. . 3 ⊢ (𝜑 → 𝐾 = (topGen‘{𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))}))
76	3	feqmptd 6735	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘)))
77	76	fveq2d 6676	. . . . 5 ⊢ (𝜑 → (∏t‘𝐹) = (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))))
78	20, 77	syl5eq 2870	. . . 4 ⊢ (𝜑 → 𝐾 = (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))))
79	6	ralrimiva 3184	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘)))
80		eqid 2823	. . . . . 6 ⊢ (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))) = (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘)))
81	80	pttopon 22206	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) ∈ (TopOn‘∪ (𝐹‘𝑘))) → (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))) ∈ (TopOn‘X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘)))
82	13, 79, 81	syl2anc 586	. . . 4 ⊢ (𝜑 → (∏t‘(𝑘 ∈ 𝐼 ↦ (𝐹‘𝑘))) ∈ (TopOn‘X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘)))
83	78, 82	eqeltrd 2915	. . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘)))
84	1, 75, 83, 21	tgcnp 21863	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝐷) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)):𝑋⟶X𝑘 ∈ 𝐼 ∪ (𝐹‘𝑘) ∧ ∀𝑓 ∈ {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑔‘𝑛) ∈ (𝐹‘𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼 ∖ 𝑤)(𝑔‘𝑛) = ∪ (𝐹‘𝑛)) ∧ 𝑎 = X𝑛 ∈ 𝐼 (𝑔‘𝑛))} (((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ 𝑓)))))
85	18, 70, 84	mpbir2and 711	1 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝐷))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {cab 2801  ∀wral 3140  ∃wrex 3141   ∖ cdif 3935   ⊆ wss 3938  ∪ cuni 4840   ↦ cmpt 5148   “ cima 5560   Fn wfn 6352  ⟶wf 6353  ‘cfv 6357  (class class class)co 7158  Xcixp 8463  Fincfn 8511  topGenctg 16713  ∏_tcpt 16714  Topctop 21503  TopOnctopon 21520   CnP ccnp 21835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-iin 4924  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-1st 7691  df-2nd 7692  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-oadd 8108  df-er 8291  df-map 8410  df-ixp 8464  df-en 8512  df-dom 8513  df-fin 8515  df-fi 8877  df-topgen 16719  df-pt 16720  df-top 21504  df-topon 21521  df-bases 21556  df-cnp 21838

This theorem is referenced by:  ptcn  22237