MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-hmeo Unicode version

Definition df-hmeo 19308
Description: Function returning all the homeomorphisms from topology to topology . (Contributed by FL, 14-Feb-2007.)
Assertion
Ref Expression
df-hmeo
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-hmeo
StepHypRef Expression
1 chmeo 19306 . 2
2 vj . . 3
3 vk . . 3
4 ctop 18478 . . 3
5 vf . . . . . . 7
65cv 1368 . . . . . 6
76ccnv 4834 . . . . 5
83cv 1368 . . . . . 6
92cv 1368 . . . . . 6
10 ccn 18808 . . . . . 6
118, 9, 10co 6086 . . . . 5
127, 11wcel 1756 . . . 4
139, 8, 10co 6086 . . . 4
1412, 5, 13crab 2714 . . 3
152, 3, 4, 4, 14cmpt2 6088 . 2
161, 15wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  hmeofn  19310  hmeofval  19311
  Copyright terms: Public domain W3C validator