Metamath Proof Explorer

Theorem ismtyval

Description: The set of isometries between two metric spaces. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion ismtyval 
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( M Ismty N ) = { f | ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) } )

Proof

Step Hyp Ref Expression
1 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 ) ) ) } )
2 1 a1i 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> 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 ) ) ) } ) )
3 dmeq 
 |-  ( m = M -> dom m = dom M )
4 xmetf 
 |-  ( M e. ( *Met ` X ) -> M : ( X X. X ) --> RR* )
5 4 fdmd 
 |-  ( M e. ( *Met ` X ) -> dom M = ( X X. X ) )
6 3 5 sylan9eqr 
 |-  ( ( M e. ( *Met ` X ) /\ m = M ) -> dom m = ( X X. X ) )
7 6 ad2ant2r 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> dom m = ( X X. X ) )
8 7 dmeqd 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> dom dom m = dom ( X X. X ) )
9 dmxpid 
 |-  dom ( X X. X ) = X
10 8 9 eqtrdi 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> dom dom m = X )
11 10 f1oeq2d 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> ( f : dom dom m -1-1-onto-> dom dom n <-> f : X -1-1-onto-> dom dom n ) )
12 dmeq 
 |-  ( n = N -> dom n = dom N )
13 xmetf 
 |-  ( N e. ( *Met ` Y ) -> N : ( Y X. Y ) --> RR* )
14 13 fdmd 
 |-  ( N e. ( *Met ` Y ) -> dom N = ( Y X. Y ) )
15 12 14 sylan9eqr 
 |-  ( ( N e. ( *Met ` Y ) /\ n = N ) -> dom n = ( Y X. Y ) )
16 15 ad2ant2l 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> dom n = ( Y X. Y ) )
17 16 dmeqd 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> dom dom n = dom ( Y X. Y ) )
18 dmxpid 
 |-  dom ( Y X. Y ) = Y
19 17 18 eqtrdi 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> dom dom n = Y )
20 f1oeq3 
 |-  ( dom dom n = Y -> ( f : X -1-1-onto-> dom dom n <-> f : X -1-1-onto-> Y ) )
21 19 20 syl 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> ( f : X -1-1-onto-> dom dom n <-> f : X -1-1-onto-> Y ) )
22 11 21 bitrd 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> ( f : dom dom m -1-1-onto-> dom dom n <-> f : X -1-1-onto-> Y ) )
23 oveq 
 |-  ( m = M -> ( x m y ) = ( x M y ) )
24 oveq 
 |-  ( n = N -> ( ( f ` x ) n ( f ` y ) ) = ( ( f ` x ) N ( f ` y ) ) )
25 23 24 eqeqan12d 
 |-  ( ( m = M /\ n = N ) -> ( ( x m y ) = ( ( f ` x ) n ( f ` y ) ) <-> ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) )
26 25 adantl 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> ( ( x m y ) = ( ( f ` x ) n ( f ` y ) ) <-> ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) )
27 10 26 raleqbidv 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> ( A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) ) <-> A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) )
28 10 27 raleqbidv 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> ( A. x e. dom dom m A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) ) <-> A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) )
29 22 28 anbi12d 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> ( ( 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 ) ) ) <-> ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) ) )
30 29 abbidv 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( m = M /\ n = N ) ) -> { 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 ) ) ) } = { f | ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) } )
31 fvssunirn 
 |-  ( *Met ` X ) C_ U. ran *Met
32 simpl 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> M e. ( *Met ` X ) )
33 31 32 sselid 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> M e. U. ran *Met )
34 fvssunirn 
 |-  ( *Met ` Y ) C_ U. ran *Met
35 simpr 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> N e. ( *Met ` Y ) )
36 34 35 sselid 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> N e. U. ran *Met )
37 f1of 
 |-  ( f : X -1-1-onto-> Y -> f : X --> Y )
38 37 adantr 
 |-  ( ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) -> f : X --> Y )
39 elfvdm 
 |-  ( N e. ( *Met ` Y ) -> Y e. dom *Met )
40 elfvdm 
 |-  ( M e. ( *Met ` X ) -> X e. dom *Met )
41 elmapg 
 |-  ( ( Y e. dom *Met /\ X e. dom *Met ) -> ( f e. ( Y ^m X ) <-> f : X --> Y ) )
42 39 40 41 syl2anr 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( f e. ( Y ^m X ) <-> f : X --> Y ) )
43 38 42 syl5ibr 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) -> f e. ( Y ^m X ) ) )
44 43 abssdv 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> { f | ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) } C_ ( Y ^m X ) )
45 ovex 
 |-  ( Y ^m X ) e. _V
46 45 ssex 
 |-  ( { f | ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) } C_ ( Y ^m X ) -> { f | ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) } e. _V )
47 44 46 syl 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> { f | ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) } e. _V )
48 2 30 33 36 47 ovmpod 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( M Ismty N ) = { f | ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) } )