Definition df-ismty 36667

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

Step	Hyp	Ref	Expression
1		cismty 36666	. 2 class Ismty
2		vm	. . 3 setvar 𝑚
3		vn	. . 3 setvar 𝑛
4		cxmet 20929	. . . . 5 class ∞Met
5	4	crn 5678	. . . 4 class ran ∞Met
6	5	cuni 4909	. . 3 class ∪ ran ∞Met
7	2	cv 1541	. . . . . . . 8 class 𝑚
8	7	cdm 5677	. . . . . . 7 class dom 𝑚
9	8	cdm 5677	. . . . . 6 class dom dom 𝑚
10	3	cv 1541	. . . . . . . 8 class 𝑛
11	10	cdm 5677	. . . . . . 7 class dom 𝑛
12	11	cdm 5677	. . . . . 6 class dom dom 𝑛
13		vf	. . . . . . 7 setvar 𝑓
14	13	cv 1541	. . . . . 6 class 𝑓
15	9, 12, 14	wf1o 6543	. . . . 5 wff 𝑓:dom dom 𝑚–1-1-onto→dom dom 𝑛
16		vx	. . . . . . . . . 10 setvar 𝑥
17	16	cv 1541	. . . . . . . . 9 class 𝑥
18		vy	. . . . . . . . . 10 setvar 𝑦
19	18	cv 1541	. . . . . . . . 9 class 𝑦
20	17, 19, 7	co 7409	. . . . . . . 8 class (𝑥𝑚𝑦)
21	17, 14	cfv 6544	. . . . . . . . 9 class (𝑓‘𝑥)
22	19, 14	cfv 6544	. . . . . . . . 9 class (𝑓‘𝑦)
23	21, 22, 10	co 7409	. . . . . . . 8 class ((𝑓‘𝑥)𝑛(𝑓‘𝑦))
24	20, 23	wceq 1542	. . . . . . 7 wff (𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦))
25	24, 18, 9	wral 3062	. . . . . 6 wff ∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦))
26	25, 16, 9	wral 3062	. . . . 5 wff ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦))
27	15, 26	wa 397	. . . 4 wff (𝑓:dom dom 𝑚–1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))
28	27, 13	cab 2710	. . 3 class {𝑓 ∣ (𝑓:dom dom 𝑚–1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))}
29	2, 3, 6, 6, 28	cmpo 7411	. 2 class (𝑚 ∈ ∪ ran ∞Met, 𝑛 ∈ ∪ ran ∞Met ↦ {𝑓 ∣ (𝑓:dom dom 𝑚–1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))})
30	1, 29	wceq 1542	1 wff Ismty = (𝑚 ∈ ∪ ran ∞Met, 𝑛 ∈ ∪ ran ∞Met ↦ {𝑓 ∣ (𝑓:dom dom 𝑚–1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))})

This definition is referenced by:  ismtyval  36668