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 20842
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 20839 . 2 class CnP
2 vj . . 3 setvar 𝑗
3 vk . . 3 setvar 𝑘
4 ctop 20517 . . 3 class Top
5 vx . . . 4 setvar 𝑥
62cv 1474 . . . . 5 class 𝑗
76cuni 4372 . . . 4 class 𝑗
85cv 1474 . . . . . . . . 9 class 𝑥
9 vf . . . . . . . . . 10 setvar 𝑓
109cv 1474 . . . . . . . . 9 class 𝑓
118, 10cfv 5804 . . . . . . . 8 class (𝑓𝑥)
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1474 . . . . . . . 8 class 𝑦
1411, 13wcel 1977 . . . . . . 7 wff (𝑓𝑥) ∈ 𝑦
15 vg . . . . . . . . . 10 setvar 𝑔
165, 15wel 1978 . . . . . . . . 9 wff 𝑥𝑔
1715cv 1474 . . . . . . . . . . 11 class 𝑔
1810, 17cima 5041 . . . . . . . . . 10 class (𝑓𝑔)
1918, 13wss 3540 . . . . . . . . 9 wff (𝑓𝑔) ⊆ 𝑦
2016, 19wa 383 . . . . . . . 8 wff (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦)
2120, 15, 6wrex 2897 . . . . . . 7 wff 𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦)
2214, 21wi 4 . . . . . 6 wff ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))
233cv 1474 . . . . . 6 class 𝑘
2422, 12, 23wral 2896 . . . . 5 wff 𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))
2523cuni 4372 . . . . . 6 class 𝑘
26 cmap 7744 . . . . . 6 class 𝑚
2725, 7, 26co 6549 . . . . 5 class ( 𝑘𝑚 𝑗)
2824, 9, 27crab 2900 . . . 4 class {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}
295, 7, 28cmpt 4643 . . 3 class (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))})
302, 3, 4, 4, 29cmpt2 6551 . 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
311, 30wceq 1475 1 wff CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
Colors of variables: wff setvar class
This definition is referenced by:  cnpfval  20848  iscnp2  20853
  Copyright terms: Public domain W3C validator