Metamath Proof Explorer

Definition df-bj-tophom

Description: Define the set of continuous functions (morphisms of topological spaces) between two topological spaces. Similar to df-cn (which is in terms of topologies instead of topological spaces). (Contributed by BJ, 10-Feb-2022)

Ref Expression
Assertion df-bj-tophom ⊢ ⟶Top = x ∈ TopSp , y ∈ TopSp ⟼ f ∈ Base x ⟶Set Base y | ∀ u ∈ TopOpen ⁡ y f -1 u ∈ TopOpen ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctophom class ⟶Top
1 vx setvar x
2 ctps class TopSp
3 vy setvar y
4 vf setvar f
5 cbs class Base
6 1 cv setvar x
7 6 5 cfv class Base x
8 csethom class ⟶Set
9 3 cv setvar y
10 9 5 cfv class Base y
11 7 10 8 co class Base x ⟶Set Base y
12 vu setvar u
13 ctopn class TopOpen
14 9 13 cfv class TopOpen ⁡ y
15 4 cv setvar f
16 15 ccnv class f -1
17 12 cv setvar u
18 16 17 cima class f -1 u
19 6 13 cfv class TopOpen ⁡ x
20 18 19 wcel wff f -1 u ∈ TopOpen ⁡ x
21 20 12 14 wral wff ∀ u ∈ TopOpen ⁡ y f -1 u ∈ TopOpen ⁡ x
22 21 4 11 crab class f ∈ Base x ⟶Set Base y | ∀ u ∈ TopOpen ⁡ y f -1 u ∈ TopOpen ⁡ x
23 1 3 2 2 22 cmpo class x ∈ TopSp , y ∈ TopSp ⟼ f ∈ Base x ⟶Set Base y | ∀ u ∈ TopOpen ⁡ y f -1 u ∈ TopOpen ⁡ x
24 0 23 wceq wff ⟶Top = x ∈ TopSp , y ∈ TopSp ⟼ f ∈ Base x ⟶Set Base y | ∀ u ∈ TopOpen ⁡ y f -1 u ∈ TopOpen ⁡ x