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 = j ∈ Top , k ∈ Top ⟼ x ∈ ⋃ j ⟼ f ∈ ⋃ k ⋃ j | ∀ y ∈ k f ⁡ x ∈ y → ∃ g ∈ j x ∈ g ∧ f g ⊆ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnp class CnP
1 vj setvar j
2 ctop class Top
3 vk setvar k
4 vx setvar x
5 1 cv setvar j
6 5 cuni class ⋃ j
7 vf setvar f
8 3 cv setvar k
9 8 cuni class ⋃ k
10 cmap class ↑ 𝑚
11 9 6 10 co class ⋃ k ⋃ j
12 vy setvar y
13 7 cv setvar f
14 4 cv setvar x
15 14 13 cfv class f ⁡ x
16 12 cv setvar y
17 15 16 wcel wff f ⁡ x ∈ y
18 vg setvar g
19 18 cv setvar g
20 14 19 wcel wff x ∈ g
21 13 19 cima class f g
22 21 16 wss wff f g ⊆ y
23 20 22 wa wff x ∈ g ∧ f g ⊆ y
24 23 18 5 wrex wff ∃ g ∈ j x ∈ g ∧ f g ⊆ y
25 17 24 wi wff f ⁡ x ∈ y → ∃ g ∈ j x ∈ g ∧ f g ⊆ y
26 25 12 8 wral wff ∀ y ∈ k f ⁡ x ∈ y → ∃ g ∈ j x ∈ g ∧ f g ⊆ y
27 26 7 11 crab class f ∈ ⋃ k ⋃ j | ∀ y ∈ k f ⁡ x ∈ y → ∃ g ∈ j x ∈ g ∧ f g ⊆ y
28 4 6 27 cmpt class x ∈ ⋃ j ⟼ f ∈ ⋃ k ⋃ j | ∀ y ∈ k f ⁡ x ∈ y → ∃ g ∈ j x ∈ g ∧ f g ⊆ y
29 1 3 2 2 28 cmpo class j ∈ Top , k ∈ Top ⟼ x ∈ ⋃ j ⟼ f ∈ ⋃ k ⋃ j | ∀ y ∈ k f ⁡ x ∈ y → ∃ g ∈ j x ∈ g ∧ f g ⊆ y
30 0 29 wceq wff CnP = j ∈ Top , k ∈ Top ⟼ x ∈ ⋃ j ⟼ f ∈ ⋃ k ⋃ j | ∀ y ∈ k f ⁡ x ∈ y → ∃ g ∈ j x ∈ g ∧ f g ⊆ y