MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cnp Structured version   Visualization version   GIF version

Definition df-cnp 21766
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
StepHypRef Expression
1 ccnp 21763 . 2 class CnP
2 vj . . 3 setvar 𝑗
3 vk . . 3 setvar 𝑘
4 ctop 21431 . . 3 class Top
5 vx . . . 4 setvar 𝑥
62cv 1527 . . . . 5 class 𝑗
76cuni 4832 . . . 4 class 𝑗
85cv 1527 . . . . . . . . 9 class 𝑥
9 vf . . . . . . . . . 10 setvar 𝑓
109cv 1527 . . . . . . . . 9 class 𝑓
118, 10cfv 6349 . . . . . . . 8 class (𝑓𝑥)
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1527 . . . . . . . 8 class 𝑦
1411, 13wcel 2105 . . . . . . 7 wff (𝑓𝑥) ∈ 𝑦
15 vg . . . . . . . . . 10 setvar 𝑔
165, 15wel 2106 . . . . . . . . 9 wff 𝑥𝑔
1715cv 1527 . . . . . . . . . . 11 class 𝑔
1810, 17cima 5552 . . . . . . . . . 10 class (𝑓𝑔)
1918, 13wss 3935 . . . . . . . . 9 wff (𝑓𝑔) ⊆ 𝑦
2016, 19wa 396 . . . . . . . 8 wff (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦)
2120, 15, 6wrex 3139 . . . . . . 7 wff 𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦)
2214, 21wi 4 . . . . . 6 wff ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))
233cv 1527 . . . . . 6 class 𝑘
2422, 12, 23wral 3138 . . . . 5 wff 𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))
2523cuni 4832 . . . . . 6 class 𝑘
26 cmap 8396 . . . . . 6 class m
2725, 7, 26co 7145 . . . . 5 class ( 𝑘m 𝑗)
2824, 9, 27crab 3142 . . . 4 class {𝑓 ∈ ( 𝑘m 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}
295, 7, 28cmpt 5138 . . 3 class (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘m 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))})
302, 3, 4, 4, 29cmpo 7147 . 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘m 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
311, 30wceq 1528 1 wff CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘m 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
Colors of variables: wff setvar class
This definition is referenced by:  cnpfval  21772  iscnp2  21777
  Copyright terms: Public domain W3C validator