Definition df-cnp 14425

Description: Define a function on two topologies whose value is the set of continuous mappings at a specified point in the first topology. Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.)

Assertion

Ref	Expression
df-cnp	⊢ CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}))

Distinct variable group:   𝑗,𝑘,𝑓,𝑥,𝑦,𝑔

Detailed syntax breakdown of Definition df-cnp

Step	Hyp	Ref	Expression
1		ccnp 14422	. 2 class CnP
2		vj	. . 3 setvar 𝑗
3		vk	. . 3 setvar 𝑘
4		ctop 14233	. . 3 class Top
5		vx	. . . 4 setvar 𝑥
6	2	cv 1363	. . . . 5 class 𝑗
7	6	cuni 3839	. . . 4 class ∪ 𝑗
8	5	cv 1363	. . . . . . . . 9 class 𝑥
9		vf	. . . . . . . . . 10 setvar 𝑓
10	9	cv 1363	. . . . . . . . 9 class 𝑓
11	8, 10	cfv 5258	. . . . . . . 8 class (𝑓‘𝑥)
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1363	. . . . . . . 8 class 𝑦
14	11, 13	wcel 2167	. . . . . . 7 wff (𝑓‘𝑥) ∈ 𝑦
15		vg	. . . . . . . . . 10 setvar 𝑔
16	5, 15	wel 2168	. . . . . . . . 9 wff 𝑥 ∈ 𝑔
17	15	cv 1363	. . . . . . . . . . 11 class 𝑔
18	10, 17	cima 4666	. . . . . . . . . 10 class (𝑓 “ 𝑔)
19	18, 13	wss 3157	. . . . . . . . 9 wff (𝑓 “ 𝑔) ⊆ 𝑦
20	16, 19	wa 104	. . . . . . . 8 wff (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦)
21	20, 15, 6	wrex 2476	. . . . . . 7 wff ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦)
22	14, 21	wi 4	. . . . . 6 wff ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))
23	3	cv 1363	. . . . . 6 class 𝑘
24	22, 12, 23	wral 2475	. . . . 5 wff ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))
25	23	cuni 3839	. . . . . 6 class ∪ 𝑘
26		cmap 6707	. . . . . 6 class ↑𝑚
27	25, 7, 26	co 5922	. . . . 5 class (∪ 𝑘 ↑𝑚 ∪ 𝑗)
28	24, 9, 27	crab 2479	. . . 4 class {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}
29	5, 7, 28	cmpt 4094	. . 3 class (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))})
30	2, 3, 4, 4, 29	cmpo 5924	. 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}))
31	1, 30	wceq 1364	1 wff CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}))

This definition is referenced by:  cnpfval  14431  cnprcl2k  14442