Metamath Proof Explorer

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 ∈ Top , k ∈ Top ⟼ f ∈ j Cn k | f -1 ∈ k Cn j

Detailed syntax breakdown

Step Hyp Ref Expression
0 chmeo class Homeo
1 vj setvar j
2 ctop class Top
3 vk setvar k
4 vf setvar f
5 1 cv setvar j
6 ccn class Cn
7 3 cv setvar k
8 5 7 6 co class j Cn k
9 4 cv setvar f
10 9 ccnv class f -1
11 7 5 6 co class k Cn j
12 10 11 wcel wff f -1 ∈ k Cn j
13 12 4 8 crab class f ∈ j Cn k | f -1 ∈ k Cn j
14 1 3 2 2 13 cmpo class j ∈ Top , k ∈ Top ⟼ f ∈ j Cn k | f -1 ∈ k Cn j
15 0 14 wceq wff Homeo = j ∈ Top , k ∈ Top ⟼ f ∈ j Cn k | f -1 ∈ k Cn j