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

Definition df-ismty 26406
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 26405 . 2  class  Ismty
2 vm . . 3  set  m
3 vn . . 3  set  n
4 cxmt 16649 . . . . 5  class  * Met
54crn 4846 . . . 4  class  ran  * Met
65cuni 3983 . . 3  class  U. ran  * Met
72cv 1648 . . . . . . . 8  class  m
87cdm 4845 . . . . . . 7  class  dom  m
98cdm 4845 . . . . . 6  class  dom  dom  m
103cv 1648 . . . . . . . 8  class  n
1110cdm 4845 . . . . . . 7  class  dom  n
1211cdm 4845 . . . . . 6  class  dom  dom  n
13 vf . . . . . . 7  set  f
1413cv 1648 . . . . . 6  class  f
159, 12, 14wf1o 5420 . . . . 5  wff  f : dom  dom  m -1-1-onto-> dom  dom  n
16 vx . . . . . . . . . 10  set  x
1716cv 1648 . . . . . . . . 9  class  x
18 vy . . . . . . . . . 10  set  y
1918cv 1648 . . . . . . . . 9  class  y
2017, 19, 7co 6048 . . . . . . . 8  class  ( x m y )
2117, 14cfv 5421 . . . . . . . . 9  class  ( f `
 x )
2219, 14cfv 5421 . . . . . . . . 9  class  ( f `
 y )
2321, 22, 10co 6048 . . . . . . . 8  class  ( ( f `  x ) n ( f `  y ) )
2420, 23wceq 1649 . . . . . . 7  wff  ( x m y )  =  ( ( f `  x ) n ( f `  y ) )
2524, 18, 9wral 2674 . . . . . 6  wff  A. y  e.  dom  dom  m (
x m y )  =  ( ( f `
 x ) n ( f `  y
) )
2625, 16, 9wral 2674 . . . . 5  wff  A. x  e.  dom  dom  m A. y  e.  dom  dom  m
( x m y )  =  ( ( f `  x ) n ( f `  y ) )
2715, 26wa 359 . . . 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 2398 . . 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 6050 . 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 1649 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  26407
  Copyright terms: Public domain W3C validator