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

Definition df-cnp 21080
 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
StepHypRef Expression
1 ccnp 21077 . 2 class CnP
2 vj . . 3 setvar 𝑗
3 vk . . 3 setvar 𝑘
4 ctop 20746 . . 3 class Top
5 vx . . . 4 setvar 𝑥
62cv 1522 . . . . 5 class 𝑗
76cuni 4468 . . . 4 class 𝑗
85cv 1522 . . . . . . . . 9 class 𝑥
9 vf . . . . . . . . . 10 setvar 𝑓
109cv 1522 . . . . . . . . 9 class 𝑓
118, 10cfv 5926 . . . . . . . 8 class (𝑓𝑥)
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1522 . . . . . . . 8 class 𝑦
1411, 13wcel 2030 . . . . . . 7 wff (𝑓𝑥) ∈ 𝑦
15 vg . . . . . . . . . 10 setvar 𝑔
165, 15wel 2031 . . . . . . . . 9 wff 𝑥𝑔
1715cv 1522 . . . . . . . . . . 11 class 𝑔
1810, 17cima 5146 . . . . . . . . . 10 class (𝑓𝑔)
1918, 13wss 3607 . . . . . . . . 9 wff (𝑓𝑔) ⊆ 𝑦
2016, 19wa 383 . . . . . . . 8 wff (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦)
2120, 15, 6wrex 2942 . . . . . . 7 wff 𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦)
2214, 21wi 4 . . . . . 6 wff ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))
233cv 1522 . . . . . 6 class 𝑘
2422, 12, 23wral 2941 . . . . 5 wff 𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))
2523cuni 4468 . . . . . 6 class 𝑘
26 cmap 7899 . . . . . 6 class 𝑚
2725, 7, 26co 6690 . . . . 5 class ( 𝑘𝑚 𝑗)
2824, 9, 27crab 2945 . . . 4 class {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}
295, 7, 28cmpt 4762 . . 3 class (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))})
302, 3, 4, 4, 29cmpt2 6692 . 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
311, 30wceq 1523 1 wff CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
 Colors of variables: wff setvar class This definition is referenced by:  cnpfval  21086  iscnp2  21091
 Copyright terms: Public domain W3C validator