Definition df-ismty 33598

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 = ( m e. U. ran *Met , n e. U. ran *Met |-> { f | ( f : dom dom m -1-1-onto-> dom dom n /\ A. x e. dom dom m A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) ) ) } )

Distinct variable group:   m, n, f, x, y

Detailed syntax breakdown of Definition df-ismty

Step	Hyp	Ref	Expression
1		cismty 33597	. 2 class Ismty
2		vm	. . 3 setvar m
3		vn	. . 3 setvar n
4		cxmt 19731	. . . . 5 class *Met
5	4	crn 5115	. . . 4 class ran *Met
6	5	cuni 4436	. . 3 class U. ran *Met
7	2	cv 1482	. . . . . . . 8 class m
8	7	cdm 5114	. . . . . . 7 class dom m
9	8	cdm 5114	. . . . . 6 class dom dom m
10	3	cv 1482	. . . . . . . 8 class n
11	10	cdm 5114	. . . . . . 7 class dom n
12	11	cdm 5114	. . . . . 6 class dom dom n
13		vf	. . . . . . 7 setvar f
14	13	cv 1482	. . . . . 6 class f
15	9, 12, 14	wf1o 5887	. . . . 5 wff f : dom dom m -1-1-onto-> dom dom n
16		vx	. . . . . . . . . 10 setvar x
17	16	cv 1482	. . . . . . . . 9 class x
18		vy	. . . . . . . . . 10 setvar y
19	18	cv 1482	. . . . . . . . 9 class y
20	17, 19, 7	co 6650	. . . . . . . 8 class ( x m y )
21	17, 14	cfv 5888	. . . . . . . . 9 class ( f ` x )
22	19, 14	cfv 5888	. . . . . . . . 9 class ( f ` y )
23	21, 22, 10	co 6650	. . . . . . . 8 class ( ( f ` x ) n ( f ` y ) )
24	20, 23	wceq 1483	. . . . . . 7 wff ( x m y ) = ( ( f ` x ) n ( f ` y ) )
25	24, 18, 9	wral 2912	. . . . . 6 wff A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) )
26	25, 16, 9	wral 2912	. . . . 5 wff A. x e. dom dom m A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) )
27	15, 26	wa 384	. . . 4 wff ( f : dom dom m -1-1-onto-> dom dom n /\ A. x e. dom dom m A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) ) )
28	27, 13	cab 2608	. . 3 class { f | ( f : dom dom m -1-1-onto-> dom dom n /\ A. x e. dom dom m A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) ) ) }
29	2, 3, 6, 6, 28	cmpt2 6652	. 2 class ( m e. U. ran *Met , n e. U. ran *Met |-> { f | ( f : dom dom m -1-1-onto-> dom dom n /\ A. x e. dom dom m A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) ) ) } )
30	1, 29	wceq 1483	1 wff Ismty = ( m e. U. ran *Met , n e. U. ran *Met |-> { f | ( f : dom dom m -1-1-onto-> dom dom n /\ A. x e. dom dom m A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) ) ) } )

This definition is referenced by:  ismtyval  33599