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 e. TopSp , y e. TopSp |-> { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( TopOpen ` y ) ( `' f " u ) e. ( TopOpen ` x ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctophom	|- -Top->
1		vx	|- x
2		ctps	|- TopSp
3		vy	|- y
4		vf	|- f
5		cbs	|- Base
6	1	cv	|- x
7	6 5	cfv	|- ( Base ` x )
8		csethom	|- -Set->
9	3	cv	|- y
10	9 5	cfv	|- ( Base ` y )
11	7 10 8	co	|- ( ( Base ` x ) -Set-> ( Base ` y ) )
12		vu	|- u
13		ctopn	|- TopOpen
14	9 13	cfv	|- ( TopOpen ` y )
15	4	cv	|- f
16	15	ccnv	|- `' f
17	12	cv	|- u
18	16 17	cima	|- ( `' f " u )
19	6 13	cfv	|- ( TopOpen ` x )
20	18 19	wcel	|- ( `' f " u ) e. ( TopOpen ` x )
21	20 12 14	wral	|- A. u e. ( TopOpen ` y ) ( `' f " u ) e. ( TopOpen ` x )
22	21 4 11	crab	|- { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( TopOpen ` y ) ( `' f " u ) e. ( TopOpen ` x ) }
23	1 3 2 2 22	cmpo	|- ( x e. TopSp , y e. TopSp |-> { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( TopOpen ` y ) ( `' f " u ) e. ( TopOpen ` x ) } )
24	0 23	wceq	|- -Top-> = ( x e. TopSp , y e. TopSp |-> { f e. ( ( Base ` x ) -Set-> ( Base ` y ) ) | A. u e. ( TopOpen ` y ) ( `' f " u ) e. ( TopOpen ` x ) } )