Definition df-ismty

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)

	Ref	Expression
Assertion	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 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cismty	|- Ismty
1		vm	|- m
2		cxmet	|- *Met
3	2	crn	|- ran *Met
4	3	cuni	|- U. ran *Met
5		vn	|- n
6		vf	|- f
7	6	cv	|- f
8	1	cv	|- m
9	8	cdm	|- dom m
10	9	cdm	|- dom dom m
11	5	cv	|- n
12	11	cdm	|- dom n
13	12	cdm	|- dom dom n
14	10 13 7	wf1o	|- f : dom dom m -1-1-onto-> dom dom n
15		vx	|- x
16		vy	|- y
17	15	cv	|- x
18	16	cv	|- y
19	17 18 8	co	|- ( x m y )
20	17 7	cfv	|- ( f ` x )
21	18 7	cfv	|- ( f ` y )
22	20 21 11	co	|- ( ( f ` x ) n ( f ` y ) )
23	19 22	wceq	|- ( x m y ) = ( ( f ` x ) n ( f ` y ) )
24	23 16 10	wral	|- A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) )
25	24 15 10	wral	|- A. x e. dom dom m A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) )
26	14 25	wa	|- ( 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 ) ) )
27	26 6	cab	|- { 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 ) ) ) }
28	1 5 4 4 27	cmpo	|- ( 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 ) ) ) } )
29	0 28	wceq	|- 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 ) ) ) } )