This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cnp

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)

Ref Expression
Assertion df-cnp CnP = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnp ⊢ CnP
1 vj ⊢ 𝑗
2 ctop ⊢ Top
3 vk ⊢ 𝑘
4 vx ⊢ 𝑥
5 1 cv ⊢ 𝑗
6 5 cuni ⊢ ∪ 𝑗
7 vf ⊢ 𝑓
8 3 cv ⊢ 𝑘
9 8 cuni ⊢ ∪ 𝑘
10 cmap ⊢ ↑m
11 9 6 10 co ⊢ ( ∪ 𝑘 ↑m ∪ 𝑗 )
12 vy ⊢ 𝑦
13 7 cv ⊢ 𝑓
14 4 cv ⊢ 𝑥
15 14 13 cfv ⊢ ( 𝑓 ‘ 𝑥 )
16 12 cv ⊢ 𝑦
17 15 16 wcel ⊢ ( 𝑓 ‘ 𝑥 ) ∈ 𝑦
18 vg ⊢ 𝑔
19 18 cv ⊢ 𝑔
20 14 19 wcel ⊢ 𝑥 ∈ 𝑔
21 13 19 cima ⊢ ( 𝑓 “ 𝑔 )
22 21 16 wss ⊢ ( 𝑓 “ 𝑔 ) ⊆ 𝑦
23 20 22 wa ⊢ ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 )
24 23 18 5 wrex ⊢ ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 )
25 17 24 wi ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) )
26 25 12 8 wral ⊢ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) )
27 26 7 11 crab ⊢ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) }
28 4 6 27 cmpt ⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } )
29 1 3 2 2 28 cmpo ⊢ ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) )
30 0 29 wceq ⊢ CnP = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) )