Metamath Proof Explorer

Theorem imasf1oxms

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 )
imasf1oxms.r 
|- ( ph -> R e. *MetSp )
Assertion imasf1oxms 
|- ( 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 imasf1oxms.r 
 |-  ( ph -> R e. *MetSp )
5 eqid 
 |-  ( ( dist ` R ) |` ( V X. V ) ) = ( ( dist ` R ) |` ( V X. V ) )
6 eqid 
 |-  ( dist ` U ) = ( dist ` U )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 eqid 
 |-  ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) = ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) )
9 7 8 xmsxmet 
 |-  ( R e. *MetSp -> ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) e. ( *Met ` ( Base ` R ) ) )
10 4 9 syl 
 |-  ( ph -> ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) e. ( *Met ` ( Base ` R ) ) )
11 2 sqxpeqd 
 |-  ( ph -> ( V X. V ) = ( ( Base ` R ) X. ( Base ` R ) ) )
12 11 reseq2d 
 |-  ( ph -> ( ( dist ` R ) |` ( V X. V ) ) = ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) )
13 2 fveq2d 
 |-  ( ph -> ( *Met ` V ) = ( *Met ` ( Base ` R ) ) )
14 10 12 13 3eltr4d 
 |-  ( ph -> ( ( dist ` R ) |` ( V X. V ) ) e. ( *Met ` V ) )
15 1 2 3 4 5 6 14 imasf1oxmet 
 |-  ( ph -> ( dist ` U ) e. ( *Met ` B ) )
16 f1ofo 
 |-  ( F : V -1-1-onto-> B -> F : V -onto-> B )
17 3 16 syl 
 |-  ( ph -> F : V -onto-> B )
18 1 2 17 4 imasbas 
 |-  ( ph -> B = ( Base ` U ) )
19 18 fveq2d 
 |-  ( ph -> ( *Met ` B ) = ( *Met ` ( Base ` U ) ) )
20 15 19 eleqtrd 
 |-  ( ph -> ( dist ` U ) e. ( *Met ` ( Base ` U ) ) )
21 ssid 
 |-  ( Base ` U ) C_ ( Base ` U )
22 xmetres2 
 |-  ( ( ( dist ` U ) e. ( *Met ` ( Base ` U ) ) /\ ( Base ` U ) C_ ( Base ` U ) ) -> ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) e. ( *Met ` ( Base ` U ) ) )
23 20 21 22 sylancl 
 |-  ( ph -> ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) e. ( *Met ` ( Base ` U ) ) )
24 eqid 
 |-  ( TopOpen ` R ) = ( TopOpen ` R )
25 eqid 
 |-  ( TopOpen ` U ) = ( TopOpen ` U )
26 1 2 17 4 24 25 imastopn 
 |-  ( ph -> ( TopOpen ` U ) = ( ( TopOpen ` R ) qTop F ) )
27 24 7 8 xmstopn 
 |-  ( R e. *MetSp -> ( TopOpen ` R ) = ( MetOpen ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) )
28 4 27 syl 
 |-  ( ph -> ( TopOpen ` R ) = ( MetOpen ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) )
29 12 fveq2d 
 |-  ( ph -> ( MetOpen ` ( ( dist ` R ) |` ( V X. V ) ) ) = ( MetOpen ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) )
30 28 29 eqtr4d 
 |-  ( ph -> ( TopOpen ` R ) = ( MetOpen ` ( ( dist ` R ) |` ( V X. V ) ) ) )
31 30 oveq1d 
 |-  ( ph -> ( ( TopOpen ` R ) qTop F ) = ( ( MetOpen ` ( ( dist ` R ) |` ( V X. V ) ) ) qTop F ) )
32 blbas 
 |-  ( ( ( dist ` R ) |` ( V X. V ) ) e. ( *Met ` V ) -> ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) e. TopBases )
33 14 32 syl 
 |-  ( ph -> ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) e. TopBases )
34 unirnbl 
 |-  ( ( ( dist ` R ) |` ( V X. V ) ) e. ( *Met ` V ) -> U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) = V )
35 f1oeq2 
 |-  ( U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) = V -> ( F : U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) -1-1-onto-> B <-> F : V -1-1-onto-> B ) )
36 14 34 35 3syl 
 |-  ( ph -> ( F : U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) -1-1-onto-> B <-> F : V -1-1-onto-> B ) )
37 3 36 mpbird 
 |-  ( ph -> F : U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) -1-1-onto-> B )
38 eqid 
 |-  U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) = U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) )
39 38 tgqtop 
 |-  ( ( ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) e. TopBases /\ F : U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) -1-1-onto-> B ) -> ( ( topGen ` ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) ) qTop F ) = ( topGen ` ( ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) qTop F ) ) )
40 33 37 39 syl2anc 
 |-  ( ph -> ( ( topGen ` ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) ) qTop F ) = ( topGen ` ( ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) qTop F ) ) )
41 eqid 
 |-  ( MetOpen ` ( ( dist ` R ) |` ( V X. V ) ) ) = ( MetOpen ` ( ( dist ` R ) |` ( V X. V ) ) )
42 41 mopnval 
 |-  ( ( ( dist ` R ) |` ( V X. V ) ) e. ( *Met ` V ) -> ( MetOpen ` ( ( dist ` R ) |` ( V X. V ) ) ) = ( topGen ` ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) ) )
43 14 42 syl 
 |-  ( ph -> ( MetOpen ` ( ( dist ` R ) |` ( V X. V ) ) ) = ( topGen ` ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) ) )
44 43 oveq1d 
 |-  ( ph -> ( ( MetOpen ` ( ( dist ` R ) |` ( V X. V ) ) ) qTop F ) = ( ( topGen ` ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) ) qTop F ) )
45 eqid 
 |-  ( MetOpen ` ( dist ` U ) ) = ( MetOpen ` ( dist ` U ) )
46 45 mopnval 
 |-  ( ( dist ` U ) e. ( *Met ` B ) -> ( MetOpen ` ( dist ` U ) ) = ( topGen ` ran ( ball ` ( dist ` U ) ) ) )
47 15 46 syl 
 |-  ( ph -> ( MetOpen ` ( dist ` U ) ) = ( topGen ` ran ( ball ` ( dist ` U ) ) ) )
48 xmetf 
 |-  ( ( dist ` U ) e. ( *Met ` ( Base ` U ) ) -> ( dist ` U ) : ( ( Base ` U ) X. ( Base ` U ) ) --> RR* )
49 20 48 syl 
 |-  ( ph -> ( dist ` U ) : ( ( Base ` U ) X. ( Base ` U ) ) --> RR* )
50 ffn 
 |-  ( ( dist ` U ) : ( ( Base ` U ) X. ( Base ` U ) ) --> RR* -> ( dist ` U ) Fn ( ( Base ` U ) X. ( Base ` U ) ) )
51 fnresdm 
 |-  ( ( dist ` U ) Fn ( ( Base ` U ) X. ( Base ` U ) ) -> ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) = ( dist ` U ) )
52 49 50 51 3syl 
 |-  ( ph -> ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) = ( dist ` U ) )
53 52 fveq2d 
 |-  ( ph -> ( MetOpen ` ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) ) = ( MetOpen ` ( dist ` U ) ) )
54 3 ad2antrr 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> F : V -1-1-onto-> B )
55 f1of1 
 |-  ( F : V -1-1-onto-> B -> F : V -1-1-> B )
56 54 55 syl 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> F : V -1-1-> B )
57 cnvimass 
 |-  ( `' F " x ) C_ dom F
58 f1odm 
 |-  ( F : V -1-1-onto-> B -> dom F = V )
59 54 58 syl 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> dom F = V )
60 57 59 sseqtrid 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> ( `' F " x ) C_ V )
61 14 ad2antrr 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> ( ( dist ` R ) |` ( V X. V ) ) e. ( *Met ` V ) )
62 simprl 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> y e. V )
63 simprr 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> r e. RR* )
64 blssm 
 |-  ( ( ( ( dist ` R ) |` ( V X. V ) ) e. ( *Met ` V ) /\ y e. V /\ r e. RR* ) -> ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) C_ V )
65 61 62 63 64 syl3anc 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) C_ V )
66 f1imaeq 
 |-  ( ( F : V -1-1-> B /\ ( ( `' F " x ) C_ V /\ ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) C_ V ) ) -> ( ( F " ( `' F " x ) ) = ( F " ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) ) <-> ( `' F " x ) = ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) ) )
67 56 60 65 66 syl12anc 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> ( ( F " ( `' F " x ) ) = ( F " ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) ) <-> ( `' F " x ) = ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) ) )
68 54 16 syl 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> F : V -onto-> B )
69 simplr 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> x C_ B )
70 foimacnv 
 |-  ( ( F : V -onto-> B /\ x C_ B ) -> ( F " ( `' F " x ) ) = x )
71 68 69 70 syl2anc 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> ( F " ( `' F " x ) ) = x )
72 1 ad2antrr 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> U = ( F "s R ) )
73 2 ad2antrr 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> V = ( Base ` R ) )
74 4 ad2antrr 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> R e. *MetSp )
75 72 73 54 74 5 6 61 62 63 imasf1obl 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> ( ( F ` y ) ( ball ` ( dist ` U ) ) r ) = ( F " ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) ) )
76 75 eqcomd 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> ( F " ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) ) = ( ( F ` y ) ( ball ` ( dist ` U ) ) r ) )
77 71 76 eqeq12d 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> ( ( F " ( `' F " x ) ) = ( F " ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) ) <-> x = ( ( F ` y ) ( ball ` ( dist ` U ) ) r ) ) )
78 67 77 bitr3d 
 |-  ( ( ( ph /\ x C_ B ) /\ ( y e. V /\ r e. RR* ) ) -> ( ( `' F " x ) = ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) <-> x = ( ( F ` y ) ( ball ` ( dist ` U ) ) r ) ) )
79 78 2rexbidva 
 |-  ( ( ph /\ x C_ B ) -> ( E. y e. V E. r e. RR* ( `' F " x ) = ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) <-> E. y e. V E. r e. RR* x = ( ( F ` y ) ( ball ` ( dist ` U ) ) r ) ) )
80 3 adantr 
 |-  ( ( ph /\ x C_ B ) -> F : V -1-1-onto-> B )
81 f1ofn 
 |-  ( F : V -1-1-onto-> B -> F Fn V )
82 oveq1 
 |-  ( z = ( F ` y ) -> ( z ( ball ` ( dist ` U ) ) r ) = ( ( F ` y ) ( ball ` ( dist ` U ) ) r ) )
83 82 eqeq2d 
 |-  ( z = ( F ` y ) -> ( x = ( z ( ball ` ( dist ` U ) ) r ) <-> x = ( ( F ` y ) ( ball ` ( dist ` U ) ) r ) ) )
84 83 rexbidv 
 |-  ( z = ( F ` y ) -> ( E. r e. RR* x = ( z ( ball ` ( dist ` U ) ) r ) <-> E. r e. RR* x = ( ( F ` y ) ( ball ` ( dist ` U ) ) r ) ) )
85 84 rexrn 
 |-  ( F Fn V -> ( E. z e. ran F E. r e. RR* x = ( z ( ball ` ( dist ` U ) ) r ) <-> E. y e. V E. r e. RR* x = ( ( F ` y ) ( ball ` ( dist ` U ) ) r ) ) )
86 80 81 85 3syl 
 |-  ( ( ph /\ x C_ B ) -> ( E. z e. ran F E. r e. RR* x = ( z ( ball ` ( dist ` U ) ) r ) <-> E. y e. V E. r e. RR* x = ( ( F ` y ) ( ball ` ( dist ` U ) ) r ) ) )
87 forn 
 |-  ( F : V -onto-> B -> ran F = B )
88 80 16 87 3syl 
 |-  ( ( ph /\ x C_ B ) -> ran F = B )
89 88 rexeqdv 
 |-  ( ( ph /\ x C_ B ) -> ( E. z e. ran F E. r e. RR* x = ( z ( ball ` ( dist ` U ) ) r ) <-> E. z e. B E. r e. RR* x = ( z ( ball ` ( dist ` U ) ) r ) ) )
90 79 86 89 3bitr2d 
 |-  ( ( ph /\ x C_ B ) -> ( E. y e. V E. r e. RR* ( `' F " x ) = ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) <-> E. z e. B E. r e. RR* x = ( z ( ball ` ( dist ` U ) ) r ) ) )
91 14 adantr 
 |-  ( ( ph /\ x C_ B ) -> ( ( dist ` R ) |` ( V X. V ) ) e. ( *Met ` V ) )
92 blrn 
 |-  ( ( ( dist ` R ) |` ( V X. V ) ) e. ( *Met ` V ) -> ( ( `' F " x ) e. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) <-> E. y e. V E. r e. RR* ( `' F " x ) = ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) ) )
93 91 92 syl 
 |-  ( ( ph /\ x C_ B ) -> ( ( `' F " x ) e. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) <-> E. y e. V E. r e. RR* ( `' F " x ) = ( y ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) r ) ) )
94 15 adantr 
 |-  ( ( ph /\ x C_ B ) -> ( dist ` U ) e. ( *Met ` B ) )
95 blrn 
 |-  ( ( dist ` U ) e. ( *Met ` B ) -> ( x e. ran ( ball ` ( dist ` U ) ) <-> E. z e. B E. r e. RR* x = ( z ( ball ` ( dist ` U ) ) r ) ) )
96 94 95 syl 
 |-  ( ( ph /\ x C_ B ) -> ( x e. ran ( ball ` ( dist ` U ) ) <-> E. z e. B E. r e. RR* x = ( z ( ball ` ( dist ` U ) ) r ) ) )
97 90 93 96 3bitr4d 
 |-  ( ( ph /\ x C_ B ) -> ( ( `' F " x ) e. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) <-> x e. ran ( ball ` ( dist ` U ) ) ) )
98 97 pm5.32da 
 |-  ( ph -> ( ( x C_ B /\ ( `' F " x ) e. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) ) <-> ( x C_ B /\ x e. ran ( ball ` ( dist ` U ) ) ) ) )
99 f1ofo 
 |-  ( F : U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) -1-1-onto-> B -> F : U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) -onto-> B )
100 37 99 syl 
 |-  ( ph -> F : U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) -onto-> B )
101 38 elqtop2 
 |-  ( ( ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) e. TopBases /\ F : U. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) -onto-> B ) -> ( x e. ( ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) qTop F ) <-> ( x C_ B /\ ( `' F " x ) e. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) ) ) )
102 33 100 101 syl2anc 
 |-  ( ph -> ( x e. ( ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) qTop F ) <-> ( x C_ B /\ ( `' F " x ) e. ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) ) ) )
103 blf 
 |-  ( ( dist ` U ) e. ( *Met ` B ) -> ( ball ` ( dist ` U ) ) : ( B X. RR* ) --> ~P B )
104 frn 
 |-  ( ( ball ` ( dist ` U ) ) : ( B X. RR* ) --> ~P B -> ran ( ball ` ( dist ` U ) ) C_ ~P B )
105 15 103 104 3syl 
 |-  ( ph -> ran ( ball ` ( dist ` U ) ) C_ ~P B )
106 105 sseld 
 |-  ( ph -> ( x e. ran ( ball ` ( dist ` U ) ) -> x e. ~P B ) )
107 elpwi 
 |-  ( x e. ~P B -> x C_ B )
108 106 107 syl6 
 |-  ( ph -> ( x e. ran ( ball ` ( dist ` U ) ) -> x C_ B ) )
109 108 pm4.71rd 
 |-  ( ph -> ( x e. ran ( ball ` ( dist ` U ) ) <-> ( x C_ B /\ x e. ran ( ball ` ( dist ` U ) ) ) ) )
110 98 102 109 3bitr4d 
 |-  ( ph -> ( x e. ( ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) qTop F ) <-> x e. ran ( ball ` ( dist ` U ) ) ) )
111 110 eqrdv 
 |-  ( ph -> ( ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) qTop F ) = ran ( ball ` ( dist ` U ) ) )
112 111 fveq2d 
 |-  ( ph -> ( topGen ` ( ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) qTop F ) ) = ( topGen ` ran ( ball ` ( dist ` U ) ) ) )
113 47 53 112 3eqtr4d 
 |-  ( ph -> ( MetOpen ` ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) ) = ( topGen ` ( ran ( ball ` ( ( dist ` R ) |` ( V X. V ) ) ) qTop F ) ) )
114 40 44 113 3eqtr4d 
 |-  ( ph -> ( ( MetOpen ` ( ( dist ` R ) |` ( V X. V ) ) ) qTop F ) = ( MetOpen ` ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) ) )
115 26 31 114 3eqtrd 
 |-  ( ph -> ( TopOpen ` U ) = ( MetOpen ` ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) ) )
116 eqid 
 |-  ( Base ` U ) = ( Base ` U )
117 eqid 
 |-  ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) = ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) )
118 25 116 117 isxms2 
 |-  ( U e. *MetSp <-> ( ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) e. ( *Met ` ( Base ` U ) ) /\ ( TopOpen ` U ) = ( MetOpen ` ( ( dist ` U ) |` ( ( Base ` U ) X. ( Base ` U ) ) ) ) ) )
119 23 115 118 sylanbrc 
 |-  ( ph -> U e. *MetSp )