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	$$⊢\mathrm{Homeo}=\left(j\in \mathrm{Top},k\in \mathrm{Top}⟼\left\{f\in \left(j\mathrm{Cn}k\right)|f^{-1}\in \left(k\mathrm{Cn}j\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chmeo	$$class\mathrm{Homeo}$$
1		vj	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		vk	$$setvark$$
4		vf	$$setvarf$$
5	1	cv	$$setvarj$$
6		ccn	$$class\mathrm{Cn}$$
7	3	cv	$$setvark$$
8	5 7 6	co	$$class\left(j\mathrm{Cn}k\right)$$
9	4	cv	$$setvarf$$
10	9	ccnv	$$class{f}^{-1}$$
11	7 5 6	co	$$class\left(k\mathrm{Cn}j\right)$$
12	10 11	wcel	$$wff{f}^{-1}\in \left(k\mathrm{Cn}j\right)$$
13	12 4 8	crab	$$class\left\{f\in \left(j\mathrm{Cn}k\right)|f^{-1}\in \left(k\mathrm{Cn}j\right)\right\}$$
14	1 3 2 2 13	cmpo	$$class\left(j\in \mathrm{Top},k\in \mathrm{Top}⟼\left\{f\in \left(j\mathrm{Cn}k\right)|f^{-1}\in \left(k\mathrm{Cn}j\right)\right\}\right)$$
15	0 14	wceq	$$wff\mathrm{Homeo}=\left(j\in \mathrm{Top},k\in \mathrm{Top}⟼\left\{f\in \left(j\mathrm{Cn}k\right)|f^{-1}\in \left(k\mathrm{Cn}j\right)\right\}\right)$$