Definition df-bj-tophom 38012

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

Assertion

Ref	Expression
df-bj-tophom	⊢ Top⟶ = (𝑥 ∈ TopSp, 𝑦 ∈ TopSp ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)})

Distinct variable group:   𝑥,𝑓,𝑦,𝑢

Detailed syntax breakdown of Definition df-bj-tophom

Step	Hyp	Ref	Expression
1		ctophom 38011	. 2 class Top⟶
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		ctps 23230	. . 3 class TopSp
5		vf	. . . . . . . . 9 setvar 𝑓
6	5	cv 1569	. . . . . . . 8 class 𝑓
7	6	ccnv 5650	. . . . . . 7 class ◡𝑓
8		vu	. . . . . . . 8 setvar 𝑢
9	8	cv 1569	. . . . . . 7 class 𝑢
10	7, 9	cima 5654	. . . . . 6 class (◡𝑓 “ 𝑢)
11	2	cv 1569	. . . . . . 7 class 𝑥
12		ctopn 17572	. . . . . . 7 class TopOpen
13	11, 12	cfv 6531	. . . . . 6 class (TopOpen‘𝑥)
14	10, 13	wcel 2145	. . . . 5 wff (◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)
15	3	cv 1569	. . . . . 6 class 𝑦
16	15, 12	cfv 6531	. . . . 5 class (TopOpen‘𝑦)
17	14, 8, 16	wral 3077	. . . 4 wff ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)
18		cbs 17367	. . . . . 6 class Base
19	11, 18	cfv 6531	. . . . 5 class (Base‘𝑥)
20	15, 18	cfv 6531	. . . . 5 class (Base‘𝑦)
21		csethom 38009	. . . . 5 class Set⟶
22	19, 20, 21	co 7412	. . . 4 class ((Base‘𝑥) Set⟶ (Base‘𝑦))
23	17, 5, 22	crab 3413	. . 3 class {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)}
24	2, 3, 4, 4, 23	cmpo 7414	. 2 class (𝑥 ∈ TopSp, 𝑦 ∈ TopSp ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)})
25	1, 24	wceq 1570	1 wff Top⟶ = (𝑥 ∈ TopSp, 𝑦 ∈ TopSp ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)})

This definition is used by: (None)