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

Definition df-ismty 28838
 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 28837 . 2
2 vm . . 3
3 vn . . 3
4 cxmt 17912 . . . . 5
54crn 4941 . . . 4
65cuni 4191 . . 3
72cv 1369 . . . . . . . 8
87cdm 4940 . . . . . . 7
98cdm 4940 . . . . . 6
103cv 1369 . . . . . . . 8
1110cdm 4940 . . . . . . 7
1211cdm 4940 . . . . . 6
13 vf . . . . . . 7
1413cv 1369 . . . . . 6
159, 12, 14wf1o 5517 . . . . 5
16 vx . . . . . . . . . 10
1716cv 1369 . . . . . . . . 9
18 vy . . . . . . . . . 10
1918cv 1369 . . . . . . . . 9
2017, 19, 7co 6192 . . . . . . . 8
2117, 14cfv 5518 . . . . . . . . 9
2219, 14cfv 5518 . . . . . . . . 9
2321, 22, 10co 6192 . . . . . . . 8
2420, 23wceq 1370 . . . . . . 7
2524, 18, 9wral 2795 . . . . . 6
2625, 16, 9wral 2795 . . . . 5
2715, 26wa 369 . . . 4
2827, 13cab 2436 . . 3
292, 3, 6, 6, 28cmpt2 6194 . 2
301, 29wceq 1370 1
 Colors of variables: wff setvar class This definition is referenced by:  ismtyval  28839
 Copyright terms: Public domain W3C validator