Definition df-hmeo

Description: Function returning all the homeomorphisms from topology j to topology k . (Contributed by FL, 14-Feb-2007)

	Ref	Expression
Assertion	df-hmeo	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chmeo	|- Homeo
1		vj	|- j
2		ctop	|- Top
3		vk	|- k
4		vf	|- f
5	1	cv	|- j
6		ccn	|- Cn
7	3	cv	|- k
8	5 7 6	co	|- ( j Cn k )
9	4	cv	|- f
10	9	ccnv	|- `' f
11	7 5 6	co	|- ( k Cn j )
12	10 11	wcel	|- `' f e. ( k Cn j )
13	12 4 8	crab	|- { f e. ( j Cn k ) | `' f e. ( k Cn j ) }
14	1 3 2 2 13	cmpo	|- ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
15	0 14	wceq	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )