ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-hmeo Unicode version

Definition df-hmeo 13056
Description: Function returning all the homeomorphisms from topology  j to topology  k. (Contributed by FL, 14-Feb-2007.)
Assertion
Ref Expression
df-hmeo  |-  Homeo  =  ( j  e.  Top , 
k  e.  Top  |->  { f  e.  ( j  Cn  k )  |  `' f  e.  (
k  Cn  j ) } )
Distinct variable group:    f, j, k

Detailed syntax breakdown of Definition df-hmeo
StepHypRef Expression
1 chmeo 13055 . 2  class  Homeo
2 vj . . 3  setvar  j
3 vk . . 3  setvar  k
4 ctop 12750 . . 3  class  Top
5 vf . . . . . . 7  setvar  f
65cv 1347 . . . . . 6  class  f
76ccnv 4608 . . . . 5  class  `' f
83cv 1347 . . . . . 6  class  k
92cv 1347 . . . . . 6  class  j
10 ccn 12940 . . . . . 6  class  Cn
118, 9, 10co 5851 . . . . 5  class  ( k  Cn  j )
127, 11wcel 2141 . . . 4  wff  `' f  e.  ( k  Cn  j )
139, 8, 10co 5851 . . . 4  class  ( j  Cn  k )
1412, 5, 13crab 2452 . . 3  class  { f  e.  ( j  Cn  k )  |  `' f  e.  ( k  Cn  j ) }
152, 3, 4, 4, 14cmpo 5853 . 2  class  ( j  e.  Top ,  k  e.  Top  |->  { f  e.  ( j  Cn  k )  |  `' f  e.  ( k  Cn  j ) } )
161, 15wceq 1348 1  wff  Homeo  =  ( j  e.  Top , 
k  e.  Top  |->  { f  e.  ( j  Cn  k )  |  `' f  e.  (
k  Cn  j ) } )
Colors of variables: wff set class
This definition is referenced by:  hmeofn  13057  hmeofvalg  13058  ishmeo  13059
  Copyright terms: Public domain W3C validator