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

Definition df-ismty 26522
 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
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-ismty
StepHypRef Expression
1 cismty 26521 . 2
2 vm . . 3
3 vn . . 3
4 cxmt 16691 . . . . 5
54crn 4882 . . . 4
65cuni 4017 . . 3
72cv 1652 . . . . . . . 8
87cdm 4881 . . . . . . 7
98cdm 4881 . . . . . 6
103cv 1652 . . . . . . . 8
1110cdm 4881 . . . . . . 7
1211cdm 4881 . . . . . 6
13 vf . . . . . . 7
1413cv 1652 . . . . . 6
159, 12, 14wf1o 5456 . . . . 5
16 vx . . . . . . . . . 10
1716cv 1652 . . . . . . . . 9
18 vy . . . . . . . . . 10
1918cv 1652 . . . . . . . . 9
2017, 19, 7co 6084 . . . . . . . 8
2117, 14cfv 5457 . . . . . . . . 9
2219, 14cfv 5457 . . . . . . . . 9
2321, 22, 10co 6084 . . . . . . . 8
2420, 23wceq 1653 . . . . . . 7
2524, 18, 9wral 2707 . . . . . 6
2625, 16, 9wral 2707 . . . . 5
2715, 26wa 360 . . . 4
2827, 13cab 2424 . . 3
292, 3, 6, 6, 28cmpt2 6086 . 2
301, 29wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  ismtyval  26523
 Copyright terms: Public domain W3C validator