Definition df-cnp 12789

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 12786	. 2 class CnP
2		vj	. . 3 setvar 𝑗
3		vk	. . 3 setvar 𝑘
4		ctop 12595	. . 3 class Top
5		vx	. . . 4 setvar 𝑥
6	2	cv 1342	. . . . 5 class 𝑗
7	6	cuni 3788	. . . 4 class ∪ 𝑗
8	5	cv 1342	. . . . . . . . 9 class 𝑥
9		vf	. . . . . . . . . 10 setvar 𝑓
10	9	cv 1342	. . . . . . . . 9 class 𝑓
11	8, 10	cfv 5187	. . . . . . . 8 class (𝑓‘𝑥)
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1342	. . . . . . . 8 class 𝑦
14	11, 13	wcel 2136	. . . . . . 7 wff (𝑓‘𝑥) ∈ 𝑦
15		vg	. . . . . . . . . 10 setvar 𝑔
16	5, 15	wel 2137	. . . . . . . . 9 wff 𝑥 ∈ 𝑔
17	15	cv 1342	. . . . . . . . . . 11 class 𝑔
18	10, 17	cima 4606	. . . . . . . . . 10 class (𝑓 “ 𝑔)
19	18, 13	wss 3115	. . . . . . . . 9 wff (𝑓 “ 𝑔) ⊆ 𝑦
20	16, 19	wa 103	. . . . . . . 8 wff (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦)
21	20, 15, 6	wrex 2444	. . . . . . 7 wff ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦)
22	14, 21	wi 4	. . . . . 6 wff ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))
23	3	cv 1342	. . . . . 6 class 𝑘
24	22, 12, 23	wral 2443	. . . . 5 wff ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))
25	23	cuni 3788	. . . . . 6 class ∪ 𝑘
26		cmap 6610	. . . . . 6 class ↑𝑚
27	25, 7, 26	co 5841	. . . . 5 class (∪ 𝑘 ↑𝑚 ∪ 𝑗)
28	24, 9, 27	crab 2447	. . . 4 class {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}
29	5, 7, 28	cmpt 4042	. . 3 class (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))})
30	2, 3, 4, 4, 29	cmpo 5843	. 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}))
31	1, 30	wceq 1343	1 wff CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}))

This definition is referenced by:  cnpfval  12795  cnprcl2k  12806