Definition df-bj-tophom 35296

Description: Define the set of continuous functions (morphisms of topological spaces) between two topological spaces. Similar to df-cn 22378 (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 35295	. 2 class Top⟶
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		ctps 22081	. . 3 class TopSp
5		vf	. . . . . . . . 9 setvar 𝑓
6	5	cv 1538	. . . . . . . 8 class 𝑓
7	6	ccnv 5588	. . . . . . 7 class ◡𝑓
8		vu	. . . . . . . 8 setvar 𝑢
9	8	cv 1538	. . . . . . 7 class 𝑢
10	7, 9	cima 5592	. . . . . 6 class (◡𝑓 “ 𝑢)
11	2	cv 1538	. . . . . . 7 class 𝑥
12		ctopn 17132	. . . . . . 7 class TopOpen
13	11, 12	cfv 6433	. . . . . 6 class (TopOpen‘𝑥)
14	10, 13	wcel 2106	. . . . 5 wff (◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)
15	3	cv 1538	. . . . . 6 class 𝑦
16	15, 12	cfv 6433	. . . . 5 class (TopOpen‘𝑦)
17	14, 8, 16	wral 3064	. . . 4 wff ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)
18		cbs 16912	. . . . . 6 class Base
19	11, 18	cfv 6433	. . . . 5 class (Base‘𝑥)
20	15, 18	cfv 6433	. . . . 5 class (Base‘𝑦)
21		csethom 35293	. . . . 5 class Set⟶
22	19, 20, 21	co 7275	. . . 4 class ((Base‘𝑥) Set⟶ (Base‘𝑦))
23	17, 5, 22	crab 3068	. . 3 class {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)}
24	2, 3, 4, 4, 23	cmpo 7277	. 2 class (𝑥 ∈ TopSp, 𝑦 ∈ TopSp ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)})
25	1, 24	wceq 1539	1 wff Top⟶ = (𝑥 ∈ TopSp, 𝑦 ∈ TopSp ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)})

This definition is referenced by: (None)