Metamath Proof Explorer

Definition df-cn

Description: Define a function on two topologies whose value is the set of continuous mappings from the first topology to the second. Based on definition of continuous function in Munkres p. 102. See iscn for the predicate form. (Contributed by NM, 17-Oct-2006)

Ref Expression
Assertion df-cn ⊢ Cn = j ∈ Top , k ∈ Top ⟼ f ∈ ⋃ k ⋃ j | ∀ y ∈ k f -1 y ∈ j

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccn class Cn
1 vj setvar j
2 ctop class Top
3 vk setvar k
4 vf setvar f
5 3 cv setvar k
6 5 cuni class ⋃ k
7 cmap class ↑ 𝑚
8 1 cv setvar j
9 8 cuni class ⋃ j
10 6 9 7 co class ⋃ k ⋃ j
11 vy setvar y
12 4 cv setvar f
13 12 ccnv class f -1
14 11 cv setvar y
15 13 14 cima class f -1 y
16 15 8 wcel wff f -1 y ∈ j
17 16 11 5 wral wff ∀ y ∈ k f -1 y ∈ j
18 17 4 10 crab class f ∈ ⋃ k ⋃ j | ∀ y ∈ k f -1 y ∈ j
19 1 3 2 2 18 cmpo class j ∈ Top , k ∈ Top ⟼ f ∈ ⋃ k ⋃ j | ∀ y ∈ k f -1 y ∈ j
20 0 19 wceq wff Cn = j ∈ Top , k ∈ Top ⟼ f ∈ ⋃ k ⋃ j | ∀ y ∈ k f -1 y ∈ j