Definition df-bj-tophom 33079

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

Assertion

Ref	Expression
df-bj-tophom	|- -Top-> = ( x e. TopSp , y e. TopSp |-> { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( TopOpen ` y ) ( `' f " u ) e. ( TopOpen ` x ) } )

Distinct variable group:   x, f, y, u

Detailed syntax breakdown of Definition df-bj-tophom

Step	Hyp	Ref	Expression
1		ctophom 33076	. 2 class -Top->
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		ctps 20736	. . 3 class TopSp
5		vf	. . . . . . . . 9 setvar f
6	5	cv 1482	. . . . . . . 8 class f
7	6	ccnv 5113	. . . . . . 7 class `' f
8		vu	. . . . . . . 8 setvar u
9	8	cv 1482	. . . . . . 7 class u
10	7, 9	cima 5117	. . . . . 6 class ( `' f " u )
11	2	cv 1482	. . . . . . 7 class x
12		ctopn 16082	. . . . . . 7 class TopOpen
13	11, 12	cfv 5888	. . . . . 6 class ( TopOpen ` x )
14	10, 13	wcel 1990	. . . . 5 wff ( `' f " u ) e. ( TopOpen ` x )
15	3	cv 1482	. . . . . 6 class y
16	15, 12	cfv 5888	. . . . 5 class ( TopOpen ` y )
17	14, 8, 16	wral 2912	. . . 4 wff A. u e. ( TopOpen ` y ) ( `' f " u ) e. ( TopOpen ` x )
18		cbs 15857	. . . . . 6 class Base
19	11, 18	cfv 5888	. . . . 5 class ( Base ` x )
20	15, 18	cfv 5888	. . . . 5 class ( Base ` y )
21		csethom 33075	. . . . 5 class -Set->
22	19, 20, 21	co 6650	. . . 4 class ( ( Base ` x ) -Set-> ( Base ` y ) )
23	17, 5, 22	crab 2916	. . 3 class { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( TopOpen ` y ) ( `' f " u ) e. ( TopOpen ` x ) }
24	2, 3, 4, 4, 23	cmpt2 6652	. 2 class ( x e. TopSp , y e. TopSp |-> { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( TopOpen ` y ) ( `' f " u ) e. ( TopOpen ` x ) } )
25	1, 24	wceq 1483	1 wff -Top-> = ( x e. TopSp , y e. TopSp |-> { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( TopOpen ` y ) ( `' f " u ) e. ( TopOpen ` x ) } )

This definition is referenced by: (None)