Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-cnp GIF version

Definition df-cnp 12264
 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 12261 . 2 class CnP
2 vj . . 3 setvar 𝑗
3 vk . . 3 setvar 𝑘
4 ctop 12070 . . 3 class Top
5 vx . . . 4 setvar 𝑥
62cv 1313 . . . . 5 class 𝑗
76cuni 3704 . . . 4 class 𝑗
85cv 1313 . . . . . . . . 9 class 𝑥
9 vf . . . . . . . . . 10 setvar 𝑓
109cv 1313 . . . . . . . . 9 class 𝑓
118, 10cfv 5091 . . . . . . . 8 class (𝑓𝑥)
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1313 . . . . . . . 8 class 𝑦
1411, 13wcel 1463 . . . . . . 7 wff (𝑓𝑥) ∈ 𝑦
15 vg . . . . . . . . . 10 setvar 𝑔
165, 15wel 1464 . . . . . . . . 9 wff 𝑥𝑔
1715cv 1313 . . . . . . . . . . 11 class 𝑔
1810, 17cima 4510 . . . . . . . . . 10 class (𝑓𝑔)
1918, 13wss 3039 . . . . . . . . 9 wff (𝑓𝑔) ⊆ 𝑦
2016, 19wa 103 . . . . . . . 8 wff (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦)
2120, 15, 6wrex 2392 . . . . . . 7 wff 𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦)
2214, 21wi 4 . . . . . 6 wff ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))
233cv 1313 . . . . . 6 class 𝑘
2422, 12, 23wral 2391 . . . . 5 wff 𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))
2523cuni 3704 . . . . . 6 class 𝑘
26 cmap 6508 . . . . . 6 class 𝑚
2725, 7, 26co 5740 . . . . 5 class ( 𝑘𝑚 𝑗)
2824, 9, 27crab 2395 . . . 4 class {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}
295, 7, 28cmpt 3957 . . 3 class (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))})
302, 3, 4, 4, 29cmpo 5742 . 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
311, 30wceq 1314 1 wff CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 ((𝑓𝑥) ∈ 𝑦 → ∃𝑔𝑗 (𝑥𝑔 ∧ (𝑓𝑔) ⊆ 𝑦))}))
 Colors of variables: wff set class This definition is referenced by:  cnpfval  12270  cnprcl2k  12281
 Copyright terms: Public domain W3C validator