Theorem cnpfval 22720

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 22714	. . 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 4921	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → ∪ 𝑗 = ∪ 𝐽)
5		toponuni 22398	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
6	5	ad2antrr 725	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → 𝑋 = ∪ 𝐽)
7	4, 6	eqtr4d 2776	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → ∪ 𝑗 = 𝑋)
8		simprr 772	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → 𝑘 = 𝐾)
9	8	unieqd 4921	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → ∪ 𝑘 = ∪ 𝐾)
10		toponuni 22398	. . . . . . 7 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾)
11	10	ad2antlr 726	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → 𝑌 = ∪ 𝐾)
12	9, 11	eqtr4d 2776	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → ∪ 𝑘 = 𝑌)
13	12, 7	oveq12d 7422	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (∪ 𝑘 ↑m ∪ 𝑗) = (𝑌 ↑m 𝑋))
14	3	rexeqdv 3327	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤) ↔ ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤)))
15	14	imbi2d 341	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤)) ↔ ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))))
16	8, 15	raleqbidv 3343	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (∀𝑤 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤)) ↔ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))))
17	13, 16	rabeqbidv 3450	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑤 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})
18	7, 17	mpteq12dv 5238	. 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽 ∧ 𝑘 = 𝐾)) → (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑤 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝑗 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}))
19		topontop 22397	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
20	19	adantr 482	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝐽 ∈ Top)
21		topontop 22397	. . 3 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
22	21	adantl 483	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝐾 ∈ Top)
23		ovex 7437	. . . . . 6 ⊢ (𝑌 ↑m 𝑋) ∈ V
24		ssrab2 4076	. . . . . 6 ⊢ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ⊆ (𝑌 ↑m 𝑋)
25	23, 24	elpwi2 5345	. . . . 5 ⊢ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ 𝒫 (𝑌 ↑m 𝑋)
26	25	a1i 11	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑥 ∈ 𝑋) → {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ 𝒫 (𝑌 ↑m 𝑋))
27	26	fmpttd 7110	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}):𝑋⟶𝒫 (𝑌 ↑m 𝑋))
28		toponmax 22410	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
29	28	adantr 482	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝑋 ∈ 𝐽)
30	23	pwex 5377	. . . 4 ⊢ 𝒫 (𝑌 ↑m 𝑋) ∈ V
31	30	a1i 11	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝒫 (𝑌 ↑m 𝑋) ∈ V)
32		fex2 7919	. . 3 ⊢ (((𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}):𝑋⟶𝒫 (𝑌 ↑m 𝑋) ∧ 𝑋 ∈ 𝐽 ∧ 𝒫 (𝑌 ↑m 𝑋) ∈ V) → (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) ∈ V)
33	27, 29, 31, 32	syl3anc 1372	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) ∈ V)
34	2, 18, 20, 22, 33	ovmpod 7555	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}))

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071  {crab 3433  Vcvv 3475   ⊆ wss 3947  𝒫 cpw 4601  ∪ cuni 4907   ↦ cmpt 5230   “ cima 5678  ⟶wf 6536  ‘cfv 6540  (class class class)co 7404   ∈ cmpo 7406   ↑_m cmap 8816  Topctop 22377  TopOnctopon 22394   CnP ccnp 22711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-top 22378  df-topon 22395  df-cnp 22714

This theorem is referenced by:  cnpval  22722  iscnp2  22725  cnambfre  36474