Metamath Proof Explorer

Theorem imasf1oms

Description: The image of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses imasf1obl.u 
|- ( ph -> U = ( F "s R ) )
imasf1obl.v 
|- ( ph -> V = ( Base ` R ) )
imasf1obl.f 
|- ( ph -> F : V -1-1-onto-> B )
imasf1oms.r 
|- ( ph -> R e. MetSp )
Assertion imasf1oms 
|- ( ph -> U e. MetSp )

Proof

Step Hyp Ref Expression
1 imasf1obl.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasf1obl.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasf1obl.f 
 |-  ( ph -> F : V -1-1-onto-> B )
4 imasf1oms.r 
 |-  ( ph -> R e. MetSp )
5 msxms 
 |-  ( R e. MetSp -> R e. *MetSp )
6 4 5 syl 
 |-  ( ph -> R e. *MetSp )
7 1 2 3 6 imasf1oxms 
 |-  ( ph -> U e. *MetSp )
8 eqid 
 |-  ( ( dist ` R ) |` ( V X. V ) ) = ( ( dist ` R ) |` ( V X. V ) )
9 eqid 
 |-  ( dist ` U ) = ( dist ` U )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 eqid 
 |-  ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) = ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) )
12 10 11 msmet 
 |-  ( R e. MetSp -> ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) e. ( Met ` ( Base ` R ) ) )
13 4 12 syl 
 |-  ( ph -> ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) e. ( Met ` ( Base ` R ) ) )
14 2 sqxpeqd 
 |-  ( ph -> ( V X. V ) = ( ( Base ` R ) X. ( Base ` R ) ) )
15 14 reseq2d 
 |-  ( ph -> ( ( dist ` R ) |` ( V X. V ) ) = ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) )
16 2 fveq2d 
 |-  ( ph -> ( Met ` V ) = ( Met ` ( Base ` R ) ) )
17 13 15 16 3eltr4d 
 |-  ( ph -> ( ( dist ` R ) |` ( V X. V ) ) e. ( Met ` V ) )
18 1 2 3 4 8 9 17 imasf1omet 
 |-  ( ph -> ( dist ` U ) e. ( Met ` B ) )
19 f1ofo 
 |-  ( F : V -1-1-onto-> B -> F : V -onto-> B )
20 3 19 syl 
 |-  ( ph -> F : V -onto-> B )
21 1 2 20 4 imasbas 
 |-  ( ph -> B = ( Base ` U ) )
22 21 fveq2d 
 |-  ( ph -> ( Met ` B ) = ( Met ` ( Base ` U ) ) )
23 18 22 eleqtrd 
 |-  ( ph -> ( dist ` U ) e. ( Met ` ( Base ` U ) ) )
24 ssid 
 |-  ( Base ` U ) C_ ( Base ` U )
25 metres2 
 |-  ( ( ( dist ` U ) e. ( Met ` ( Base ` U ) ) /\ ( Base ` U ) C_ ( Base ` U ) ) -> ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) e. ( Met ` ( Base ` U ) ) )
26 23 24 25 sylancl 
 |-  ( ph -> ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) e. ( Met ` ( Base ` U ) ) )
27 eqid 
 |-  ( TopOpen ` U ) = ( TopOpen ` U )
28 eqid 
 |-  ( Base ` U ) = ( Base ` U )
29 eqid 
 |-  ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) = ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) )
30 27 28 29 isms 
 |-  ( U e. MetSp <-> ( U e. *MetSp /\ ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) e. ( Met ` ( Base ` U ) ) ) )
31 7 26 30 sylanbrc 
 |-  ( ph -> U e. MetSp )