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 sseldi
 |-  ( ( 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 sseldi
 |-  ( ( 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 ) ) ) } )