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⟶ = ( 𝑥 ∈ TopSp , 𝑦 ∈ TopSp ↦ { 𝑓 ∈ ( ( Base ‘ 𝑥 ) Set⟶ ( Base ‘ 𝑦 ) ) ∣ ∀ 𝑢 ∈ ( TopOpen ‘ 𝑦 ) ( ◡ 𝑓 “ 𝑢 ) ∈ ( TopOpen ‘ 𝑥 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctophom	⊢ Top⟶
1		vx	⊢ 𝑥
2		ctps	⊢ TopSp
3		vy	⊢ 𝑦
4		vf	⊢ 𝑓
5		cbs	⊢ Base
6	1	cv	⊢ 𝑥
7	6 5	cfv	⊢ ( Base ‘ 𝑥 )
8		csethom	⊢ Set⟶
9	3	cv	⊢ 𝑦
10	9 5	cfv	⊢ ( Base ‘ 𝑦 )
11	7 10 8	co	⊢ ( ( Base ‘ 𝑥 ) Set⟶ ( Base ‘ 𝑦 ) )
12		vu	⊢ 𝑢
13		ctopn	⊢ TopOpen
14	9 13	cfv	⊢ ( TopOpen ‘ 𝑦 )
15	4	cv	⊢ 𝑓
16	15	ccnv	⊢ ◡ 𝑓
17	12	cv	⊢ 𝑢
18	16 17	cima	⊢ ( ◡ 𝑓 “ 𝑢 )
19	6 13	cfv	⊢ ( TopOpen ‘ 𝑥 )
20	18 19	wcel	⊢ ( ◡ 𝑓 “ 𝑢 ) ∈ ( TopOpen ‘ 𝑥 )
21	20 12 14	wral	⊢ ∀ 𝑢 ∈ ( TopOpen ‘ 𝑦 ) ( ◡ 𝑓 “ 𝑢 ) ∈ ( TopOpen ‘ 𝑥 )
22	21 4 11	crab	⊢ { 𝑓 ∈ ( ( Base ‘ 𝑥 ) Set⟶ ( Base ‘ 𝑦 ) ) ∣ ∀ 𝑢 ∈ ( TopOpen ‘ 𝑦 ) ( ◡ 𝑓 “ 𝑢 ) ∈ ( TopOpen ‘ 𝑥 ) }
23	1 3 2 2 22	cmpo	⊢ ( 𝑥 ∈ TopSp , 𝑦 ∈ TopSp ↦ { 𝑓 ∈ ( ( Base ‘ 𝑥 ) Set⟶ ( Base ‘ 𝑦 ) ) ∣ ∀ 𝑢 ∈ ( TopOpen ‘ 𝑦 ) ( ◡ 𝑓 “ 𝑢 ) ∈ ( TopOpen ‘ 𝑥 ) } )
24	0 23	wceq	⊢ Top⟶ = ( 𝑥 ∈ TopSp , 𝑦 ∈ TopSp ↦ { 𝑓 ∈ ( ( Base ‘ 𝑥 ) Set⟶ ( Base ‘ 𝑦 ) ) ∣ ∀ 𝑢 ∈ ( TopOpen ‘ 𝑦 ) ( ◡ 𝑓 “ 𝑢 ) ∈ ( TopOpen ‘ 𝑥 ) } )