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 21837
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 21834 . 2 class CnP
2 vj . . 3 setvar 𝑗
3 vk . . 3 setvar 𝑘
4 ctop 21502 . . 3 class Top
5 vx . . . 4 setvar 𝑥
62cv 1537 . . . . 5 class 𝑗
76cuni 4803 . . . 4 class 𝑗
85cv 1537 . . . . . . . . 9 class 𝑥
9 vf . . . . . . . . . 10 setvar 𝑓
109cv 1537 . . . . . . . . 9 class 𝑓
118, 10cfv 6328 . . . . . . . 8 class (𝑓𝑥)
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1537 . . . . . . . 8 class 𝑦
1411, 13wcel 2112 . . . . . . 7 wff (𝑓𝑥) ∈ 𝑦
15 vg . . . . . . . . . 10 setvar 𝑔
165, 15wel 2113 . . . . . . . . 9 wff 𝑥𝑔
1715cv 1537 . . . . . . . . . . 11 class 𝑔
1810, 17cima 5526 . . . . . . . . . 10 class (𝑓𝑔)
1918, 13wss 3884 . . . . . . . . 9 wff (𝑓𝑔) ⊆ 𝑦
2016, 19wa 399 . . . . . . . 8 wff (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦)
2120, 15, 6wrex 3110 . . . . . . 7 wff 𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦)
2214, 21wi 4 . . . . . 6 wff ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))
233cv 1537 . . . . . 6 class 𝑘
2422, 12, 23wral 3109 . . . . 5 wff 𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))
2523cuni 4803 . . . . . 6 class 𝑘
26 cmap 8393 . . . . . 6 class m
2725, 7, 26co 7139 . . . . 5 class ( 𝑘m 𝑗)
2824, 9, 27crab 3113 . . . 4 class {𝑓 ∈ ( 𝑘m 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}
295, 7, 28cmpt 5113 . . 3 class (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘m 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))})
302, 3, 4, 4, 29cmpo 7141 . 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘m 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
311, 30wceq 1538 1 wff CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘m 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
Colors of variables: wff setvar class
This definition is referenced by:  cnpfval  21843  iscnp2  21848
  Copyright terms: Public domain W3C validator