Definition df-cnp 22287

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 ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}))

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

Detailed syntax breakdown of Definition df-cnp

Step	Hyp	Ref	Expression
1		ccnp 22284	. 2 class CnP
2		vj	. . 3 setvar 𝑗
3		vk	. . 3 setvar 𝑘
4		ctop 21950	. . 3 class Top
5		vx	. . . 4 setvar 𝑥
6	2	cv 1538	. . . . 5 class 𝑗
7	6	cuni 4836	. . . 4 class ∪ 𝑗
8	5	cv 1538	. . . . . . . . 9 class 𝑥
9		vf	. . . . . . . . . 10 setvar 𝑓
10	9	cv 1538	. . . . . . . . 9 class 𝑓
11	8, 10	cfv 6418	. . . . . . . 8 class (𝑓‘𝑥)
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1538	. . . . . . . 8 class 𝑦
14	11, 13	wcel 2108	. . . . . . 7 wff (𝑓‘𝑥) ∈ 𝑦
15		vg	. . . . . . . . . 10 setvar 𝑔
16	5, 15	wel 2109	. . . . . . . . 9 wff 𝑥 ∈ 𝑔
17	15	cv 1538	. . . . . . . . . . 11 class 𝑔
18	10, 17	cima 5583	. . . . . . . . . 10 class (𝑓 “ 𝑔)
19	18, 13	wss 3883	. . . . . . . . 9 wff (𝑓 “ 𝑔) ⊆ 𝑦
20	16, 19	wa 395	. . . . . . . 8 wff (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦)
21	20, 15, 6	wrex 3064	. . . . . . 7 wff ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦)
22	14, 21	wi 4	. . . . . 6 wff ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))
23	3	cv 1538	. . . . . 6 class 𝑘
24	22, 12, 23	wral 3063	. . . . 5 wff ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))
25	23	cuni 4836	. . . . . 6 class ∪ 𝑘
26		cmap 8573	. . . . . 6 class ↑m
27	25, 7, 26	co 7255	. . . . 5 class (∪ 𝑘 ↑m ∪ 𝑗)
28	24, 9, 27	crab 3067	. . . 4 class {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}
29	5, 7, 28	cmpt 5153	. . 3 class (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))})
30	2, 3, 4, 4, 29	cmpo 7257	. 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}))
31	1, 30	wceq 1539	1 wff CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}))

This definition is referenced by:  cnpfval  22293  iscnp2  22298