Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ismty Unicode version

Definition df-ismty 26626
Description: Define a function which takes two metric spaces and returns the set of isometries between the spaces. An isometry is a bijection which preserves distance. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
df-ismty  |-  Ismty  =  ( m  e.  U. ran  * Met ,  n  e. 
U. ran  * Met  |->  { f  |  ( f : dom  dom  m
-1-1-onto-> dom  dom  n  /\  A. x  e.  dom  dom  m A. y  e.  dom  dom  m ( x m y )  =  ( ( f `  x
) n ( f `
 y ) ) ) } )
Distinct variable group:    m, n, f, x, y

Detailed syntax breakdown of Definition df-ismty
StepHypRef Expression
1 cismty 26625 . 2  class  Ismty
2 vm . . 3  set  m
3 vn . . 3  set  n
4 cxmt 16385 . . . . 5  class  * Met
54crn 4706 . . . 4  class  ran  * Met
65cuni 3843 . . 3  class  U. ran  * Met
72cv 1631 . . . . . . . 8  class  m
87cdm 4705 . . . . . . 7  class  dom  m
98cdm 4705 . . . . . 6  class  dom  dom  m
103cv 1631 . . . . . . . 8  class  n
1110cdm 4705 . . . . . . 7  class  dom  n
1211cdm 4705 . . . . . 6  class  dom  dom  n
13 vf . . . . . . 7  set  f
1413cv 1631 . . . . . 6  class  f
159, 12, 14wf1o 5270 . . . . 5  wff  f : dom  dom  m -1-1-onto-> dom  dom  n
16 vx . . . . . . . . . 10  set  x
1716cv 1631 . . . . . . . . 9  class  x
18 vy . . . . . . . . . 10  set  y
1918cv 1631 . . . . . . . . 9  class  y
2017, 19, 7co 5874 . . . . . . . 8  class  ( x m y )
2117, 14cfv 5271 . . . . . . . . 9  class  ( f `
 x )
2219, 14cfv 5271 . . . . . . . . 9  class  ( f `
 y )
2321, 22, 10co 5874 . . . . . . . 8  class  ( ( f `  x ) n ( f `  y ) )
2420, 23wceq 1632 . . . . . . 7  wff  ( x m y )  =  ( ( f `  x ) n ( f `  y ) )
2524, 18, 9wral 2556 . . . . . 6  wff  A. y  e.  dom  dom  m (
x m y )  =  ( ( f `
 x ) n ( f `  y
) )
2625, 16, 9wral 2556 . . . . 5  wff  A. x  e.  dom  dom  m A. y  e.  dom  dom  m
( x m y )  =  ( ( f `  x ) n ( f `  y ) )
2715, 26wa 358 . . . 4  wff  ( f : dom  dom  m -1-1-onto-> dom  dom  n  /\  A. x  e.  dom  dom  m A. y  e.  dom  dom  m
( x m y )  =  ( ( f `  x ) n ( f `  y ) ) )
2827, 13cab 2282 . . 3  class  { f  |  ( f : dom  dom  m -1-1-onto-> dom  dom  n  /\  A. x  e.  dom  dom  m A. y  e.  dom  dom  m ( x m y )  =  ( ( f `  x
) n ( f `
 y ) ) ) }
292, 3, 6, 6, 28cmpt2 5876 . 2  class  ( m  e.  U. ran  * Met ,  n  e.  U. ran  * Met  |->  { f  |  ( f : dom  dom  m -1-1-onto-> dom  dom  n  /\  A. x  e.  dom  dom  m A. y  e.  dom  dom  m ( x m y )  =  ( ( f `  x
) n ( f `
 y ) ) ) } )
301, 29wceq 1632 1  wff  Ismty  =  ( m  e.  U. ran  * Met ,  n  e. 
U. ran  * Met  |->  { f  |  ( f : dom  dom  m
-1-1-onto-> dom  dom  n  /\  A. x  e.  dom  dom  m A. y  e.  dom  dom  m ( x m y )  =  ( ( f `  x
) n ( f `
 y ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  ismtyval  26627
  Copyright terms: Public domain W3C validator