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

Definition df-ismty 25935
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 25934 . 2  class  Ismty
2 vm . . 3  set  m
3 vn . . 3  set  n
4 cxmt 16369 . . . . 5  class  * Met
54crn 4690 . . . 4  class  ran  * Met
65cuni 3827 . . 3  class  U. ran  * Met
72cv 1622 . . . . . . . 8  class  m
87cdm 4689 . . . . . . 7  class  dom  m
98cdm 4689 . . . . . 6  class  dom  dom  m
103cv 1622 . . . . . . . 8  class  n
1110cdm 4689 . . . . . . 7  class  dom  n
1211cdm 4689 . . . . . 6  class  dom  dom  n
13 vf . . . . . . 7  set  f
1413cv 1622 . . . . . 6  class  f
159, 12, 14wf1o 5254 . . . . 5  wff  f : dom  dom  m -1-1-onto-> dom  dom  n
16 vx . . . . . . . . . 10  set  x
1716cv 1622 . . . . . . . . 9  class  x
18 vy . . . . . . . . . 10  set  y
1918cv 1622 . . . . . . . . 9  class  y
2017, 19, 7co 5858 . . . . . . . 8  class  ( x m y )
2117, 14cfv 5255 . . . . . . . . 9  class  ( f `
 x )
2219, 14cfv 5255 . . . . . . . . 9  class  ( f `
 y )
2321, 22, 10co 5858 . . . . . . . 8  class  ( ( f `  x ) n ( f `  y ) )
2420, 23wceq 1623 . . . . . . 7  wff  ( x m y )  =  ( ( f `  x ) n ( f `  y ) )
2524, 18, 9wral 2543 . . . . . 6  wff  A. y  e.  dom  dom  m (
x m y )  =  ( ( f `
 x ) n ( f `  y
) )
2625, 16, 9wral 2543 . . . . 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 2269 . . 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 5860 . 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 1623 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  25936
  Copyright terms: Public domain W3C validator