Users' Mathboxes 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 32564
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 32563 . 2 class Ismty
2 vm . . 3 setvar 𝑚
3 vn . . 3 setvar 𝑛
4 cxmt 19498 . . . . 5 class ∞Met
54crn 5029 . . . 4 class ran ∞Met
65cuni 4366 . . 3 class ran ∞Met
72cv 1473 . . . . . . . 8 class 𝑚
87cdm 5028 . . . . . . 7 class dom 𝑚
98cdm 5028 . . . . . 6 class dom dom 𝑚
103cv 1473 . . . . . . . 8 class 𝑛
1110cdm 5028 . . . . . . 7 class dom 𝑛
1211cdm 5028 . . . . . 6 class dom dom 𝑛
13 vf . . . . . . 7 setvar 𝑓
1413cv 1473 . . . . . 6 class 𝑓
159, 12, 14wf1o 5789 . . . . 5 wff 𝑓:dom dom 𝑚1-1-onto→dom dom 𝑛
16 vx . . . . . . . . . 10 setvar 𝑥
1716cv 1473 . . . . . . . . 9 class 𝑥
18 vy . . . . . . . . . 10 setvar 𝑦
1918cv 1473 . . . . . . . . 9 class 𝑦
2017, 19, 7co 6527 . . . . . . . 8 class (𝑥𝑚𝑦)
2117, 14cfv 5790 . . . . . . . . 9 class (𝑓𝑥)
2219, 14cfv 5790 . . . . . . . . 9 class (𝑓𝑦)
2321, 22, 10co 6527 . . . . . . . 8 class ((𝑓𝑥)𝑛(𝑓𝑦))
2420, 23wceq 1474 . . . . . . 7 wff (𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦))
2524, 18, 9wral 2895 . . . . . 6 wff 𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦))
2625, 16, 9wral 2895 . . . . 5 wff 𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦))
2715, 26wa 382 . . . 4 wff (𝑓:dom dom 𝑚1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦)))
2827, 13cab 2595 . . 3 class {𝑓 ∣ (𝑓:dom dom 𝑚1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦)))}
292, 3, 6, 6, 28cmpt2 6529 . 2 class (𝑚 ran ∞Met, 𝑛 ran ∞Met ↦ {𝑓 ∣ (𝑓:dom dom 𝑚1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓𝑥)𝑛(𝑓𝑦)))})
301, 29wceq 1474 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  32565
  Copyright terms: Public domain W3C validator