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 = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑓 ∈ ( 𝑗 Cn 𝑘 ) ∣ ◡ 𝑓 ∈ ( 𝑘 Cn 𝑗 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chmeo	⊢ Homeo
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vk	⊢ 𝑘
4		vf	⊢ 𝑓
5	1	cv	⊢ 𝑗
6		ccn	⊢ Cn
7	3	cv	⊢ 𝑘
8	5 7 6	co	⊢ ( 𝑗 Cn 𝑘 )
9	4	cv	⊢ 𝑓
10	9	ccnv	⊢ ◡ 𝑓
11	7 5 6	co	⊢ ( 𝑘 Cn 𝑗 )
12	10 11	wcel	⊢ ◡ 𝑓 ∈ ( 𝑘 Cn 𝑗 )
13	12 4 8	crab	⊢ { 𝑓 ∈ ( 𝑗 Cn 𝑘 ) ∣ ◡ 𝑓 ∈ ( 𝑘 Cn 𝑗 ) }
14	1 3 2 2 13	cmpo	⊢ ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑓 ∈ ( 𝑗 Cn 𝑘 ) ∣ ◡ 𝑓 ∈ ( 𝑘 Cn 𝑗 ) } )
15	0 14	wceq	⊢ Homeo = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑓 ∈ ( 𝑗 Cn 𝑘 ) ∣ ◡ 𝑓 ∈ ( 𝑘 Cn 𝑗 ) } )