Metamath Proof Explorer

Theorem isismty

Description: The condition "is an isometry". (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion isismty 
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) <-> ( 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 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 ) ) ) } )
2 1 eleq2d 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) <-> F e. { f | ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) } ) )
3 f1of 
 |-  ( F : X -1-1-onto-> Y -> F : X --> Y )
4 3 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 )
5 elfvdm 
 |-  ( M e. ( *Met ` X ) -> X e. dom *Met )
6 elfvdm 
 |-  ( N e. ( *Met ` Y ) -> Y e. dom *Met )
7 fex2 
 |-  ( ( F : X --> Y /\ X e. dom *Met /\ Y e. dom *Met ) -> F e. _V )
8 4 5 6 7 syl3an 
 |-  ( ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) /\ M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> F e. _V )
9 8 3expib 
 |-  ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) -> ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> F e. _V ) )
10 9 com12 
 |-  ( ( 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. _V ) )
11 f1oeq1 
 |-  ( f = F -> ( f : X -1-1-onto-> Y <-> F : X -1-1-onto-> Y ) )
12 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
13 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
14 12 13 oveq12d 
 |-  ( f = F -> ( ( f ` x ) N ( f ` y ) ) = ( ( F ` x ) N ( F ` y ) ) )
15 14 eqeq2d 
 |-  ( f = F -> ( ( x M y ) = ( ( f ` x ) N ( f ` y ) ) <-> ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) )
16 15 2ralbidv 
 |-  ( f = F -> ( A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) <-> A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) )
17 11 16 anbi12d 
 |-  ( f = F -> ( ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( 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 ) ) ) ) )
18 17 elab3g 
 |-  ( ( ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) -> F e. _V ) -> ( F e. { f | ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( 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 ) ) ) ) )
19 10 18 syl 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. { f | ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( 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 ) ) ) ) )
20 2 19 bitrd 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) <-> ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) )