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

Definition df-ismty 32768
 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 = (𝑚 ran ∞Met, 𝑛 ran ∞Met ↦ {𝑓 ∣ (𝑓:dom dom 𝑚1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦)))})
Distinct variable group:   𝑚,𝑛,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-ismty
StepHypRef Expression
1 cismty 32767 . 2 class Ismty
2 vm . . 3 setvar 𝑚
3 vn . . 3 setvar 𝑛
4 cxmt 19552 . . . . 5 class ∞Met
54crn 5039 . . . 4 class ran ∞Met
65cuni 4372 . . 3 class ran ∞Met
72cv 1474 . . . . . . . 8 class 𝑚
87cdm 5038 . . . . . . 7 class dom 𝑚
98cdm 5038 . . . . . 6 class dom dom 𝑚
103cv 1474 . . . . . . . 8 class 𝑛
1110cdm 5038 . . . . . . 7 class dom 𝑛
1211cdm 5038 . . . . . 6 class dom dom 𝑛
13 vf . . . . . . 7 setvar 𝑓
1413cv 1474 . . . . . 6 class 𝑓
159, 12, 14wf1o 5803 . . . . 5 wff 𝑓:dom dom 𝑚1-1-onto→dom dom 𝑛
16 vx . . . . . . . . . 10 setvar 𝑥
1716cv 1474 . . . . . . . . 9 class 𝑥
18 vy . . . . . . . . . 10 setvar 𝑦
1918cv 1474 . . . . . . . . 9 class 𝑦
2017, 19, 7co 6549 . . . . . . . 8 class (𝑥𝑚𝑦)
2117, 14cfv 5804 . . . . . . . . 9 class (𝑓𝑥)
2219, 14cfv 5804 . . . . . . . . 9 class (𝑓𝑦)
2321, 22, 10co 6549 . . . . . . . 8 class ((𝑓𝑥)𝑛(𝑓𝑦))
2420, 23wceq 1475 . . . . . . 7 wff (𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦))
2524, 18, 9wral 2896 . . . . . 6 wff 𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦))
2625, 16, 9wral 2896 . . . . 5 wff 𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦))
2715, 26wa 383 . . . 4 wff (𝑓:dom dom 𝑚1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦)))
2827, 13cab 2596 . . 3 class {𝑓 ∣ (𝑓:dom dom 𝑚1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦)))}
292, 3, 6, 6, 28cmpt2 6551 . 2 class (𝑚 ran ∞Met, 𝑛 ran ∞Met ↦ {𝑓 ∣ (𝑓:dom dom 𝑚1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦)))})
301, 29wceq 1475 1 wff Ismty = (𝑚 ran ∞Met, 𝑛 ran ∞Met ↦ {𝑓 ∣ (𝑓:dom dom 𝑚1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦)))})
 Colors of variables: wff setvar class This definition is referenced by:  ismtyval  32769
 Copyright terms: Public domain W3C validator