Theorem cnpfval 23149

Description: The function mapping the points in a topology 𝐽 to the set of all functions from 𝐽 to topology 𝐾 continuous at that point. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)

Assertion

Ref	Expression
cnpfval	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}))

Distinct variable groups:   𝑤,𝑓,𝑥,𝐾   𝑓,𝑋,𝑤,𝑥   𝑓,𝑌,𝑤,𝑥   𝑣,𝑓,𝐽,𝑤,𝑥

Allowed substitution hints:   𝐾(𝑣)   𝑋(𝑣)   𝑌(𝑣)

Proof of Theorem cnpfval

Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-cnp 23143	. . 3 ⊢ CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑤 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}))
2	1	a1i 11	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑤 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})))
3		simprl 770	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → 𝑗 = 𝐽)
4	3	unieqd 4869	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → ∪ 𝑗 = ∪ 𝐽)
5		toponuni 22829	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
6	5	ad2antrr 726	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → 𝑋 = ∪ 𝐽)
7	4, 6	eqtr4d 2769	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → ∪ 𝑗 = 𝑋)
8		simprr 772	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → 𝑘 = 𝐾)
9	8	unieqd 4869	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → ∪ 𝑘 = ∪ 𝐾)
10		toponuni 22829	. . . . . . 7 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾)
11	10	ad2antlr 727	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → 𝑌 = ∪ 𝐾)
12	9, 11	eqtr4d 2769	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → ∪ 𝑘 = 𝑌)
13	12, 7	oveq12d 7364	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (∪ 𝑘 ↑m ∪ 𝑗) = (𝑌 ↑m 𝑋))
14	3	rexeqdv 3293	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤) ↔ ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤)))
15	14	imbi2d 340	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤)) ↔ ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))))
16	8, 15	raleqbidv 3312	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (∀𝑤 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤)) ↔ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))))
17	13, 16	rabeqbidv 3413	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑤 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})
18	7, 17	mpteq12dv 5176	. 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑤 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}))
19		topontop 22828	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
20	19	adantr 480	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝐽 ∈ Top)
21		topontop 22828	. . 3 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
22	21	adantl 481	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝐾 ∈ Top)
23		ovex 7379	. . . . . 6 ⊢ (𝑌 ↑m 𝑋) ∈ V
24		ssrab2 4027	. . . . . 6 ⊢ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ⊆ (𝑌 ↑m 𝑋)
25	23, 24	elpwi2 5271	. . . . 5 ⊢ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ 𝒫 (𝑌 ↑m 𝑋)
26	25	a1i 11	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑥 ∈ 𝑋) → {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ 𝒫 (𝑌 ↑m 𝑋))
27	26	fmpttd 7048	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}):𝑋⟶𝒫 (𝑌 ↑m 𝑋))
28		toponmax 22841	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
29	28	adantr 480	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝑋 ∈ 𝐽)
30	23	pwex 5316	. . . 4 ⊢ 𝒫 (𝑌 ↑m 𝑋) ∈ V
31	30	a1i 11	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝒫 (𝑌 ↑m 𝑋) ∈ V)
32		fex2 7866	. . 3 ⊢ (((𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}):𝑋⟶𝒫 (𝑌 ↑m 𝑋) ∧ 𝑋 ∈ 𝐽 ∧ 𝒫 (𝑌 ↑m 𝑋) ∈ V) → (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) ∈ V)
33	27, 29, 31, 32	syl3anc 1373	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) ∈ V)
34	2, 18, 20, 22, 33	ovmpod 7498	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056  {crab 3395  Vcvv 3436   ⊆ wss 3897  𝒫 cpw 4547  ∪ cuni 4856   ↦ cmpt 5170   “ cima 5617  ⟶wf 6477  ‘cfv 6481  (class class class)co 7346   ∈ cmpo 7348   ↑_m cmap 8750  Topctop 22808  TopOnctopon 22825   CnP ccnp 23140

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-top 22809  df-topon 22826  df-cnp 23143

This theorem is referenced by:  cnpval  23151  iscnp2  23154  cnambfre  37718