Metamath Proof Explorer

Theorem isxms2

Description: Express the predicate " <. X , D >. is an extended metric space" with underlying set X and distance function D . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses isms.j 
|- J = ( TopOpen ` K )
isms.x 
|- X = ( Base ` K )
isms.d 
|- D = ( ( dist ` K ) |` ( X X. X ) )
Assertion isxms2 
|- ( K e. *MetSp <-> ( D e. ( *Met ` X ) /\ J = ( MetOpen ` D ) ) )

Proof

Step Hyp Ref Expression
1 isms.j 
 |-  J = ( TopOpen ` K )
2 isms.x 
 |-  X = ( Base ` K )
3 isms.d 
 |-  D = ( ( dist ` K ) |` ( X X. X ) )
4 1 2 3 isxms 
 |-  ( K e. *MetSp <-> ( K e. TopSp /\ J = ( MetOpen ` D ) ) )
5 2 1 istps 
 |-  ( K e. TopSp <-> J e. ( TopOn ` X ) )
6 df-mopn 
 |-  MetOpen = ( x e. U. ran *Met |-> ( topGen ` ran ( ball ` x ) ) )
7 6 dmmptss 
 |-  dom MetOpen C_ U. ran *Met
8 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
9 8 adantl 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> X e. J )
10 simpl 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> J = ( MetOpen ` D ) )
11 9 10 eleqtrd 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> X e. ( MetOpen ` D ) )
12 elfvdm 
 |-  ( X e. ( MetOpen ` D ) -> D e. dom MetOpen )
13 11 12 syl 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> D e. dom MetOpen )
14 7 13 sselid 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> D e. U. ran *Met )
15 xmetunirn 
 |-  ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )
16 14 15 sylib 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> D e. ( *Met ` dom dom D ) )
17 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
18 17 mopntopon 
 |-  ( D e. ( *Met ` dom dom D ) -> ( MetOpen ` D ) e. ( TopOn ` dom dom D ) )
19 16 18 syl 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> ( MetOpen ` D ) e. ( TopOn ` dom dom D ) )
20 10 19 eqeltrd 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> J e. ( TopOn ` dom dom D ) )
21 toponuni 
 |-  ( J e. ( TopOn ` dom dom D ) -> dom dom D = U. J )
22 20 21 syl 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> dom dom D = U. J )
23 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
24 23 adantl 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> X = U. J )
25 22 24 eqtr4d 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> dom dom D = X )
26 25 fveq2d 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> ( *Met ` dom dom D ) = ( *Met ` X ) )
27 16 26 eleqtrd 
 |-  ( ( J = ( MetOpen ` D ) /\ J e. ( TopOn ` X ) ) -> D e. ( *Met ` X ) )
28 27 ex 
 |-  ( J = ( MetOpen ` D ) -> ( J e. ( TopOn ` X ) -> D e. ( *Met ` X ) ) )
29 17 mopntopon 
 |-  ( D e. ( *Met ` X ) -> ( MetOpen ` D ) e. ( TopOn ` X ) )
30 eleq1 
 |-  ( J = ( MetOpen ` D ) -> ( J e. ( TopOn ` X ) <-> ( MetOpen ` D ) e. ( TopOn ` X ) ) )
31 29 30 imbitrrid 
 |-  ( J = ( MetOpen ` D ) -> ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) ) )
32 28 31 impbid 
 |-  ( J = ( MetOpen ` D ) -> ( J e. ( TopOn ` X ) <-> D e. ( *Met ` X ) ) )
33 5 32 bitrid 
 |-  ( J = ( MetOpen ` D ) -> ( K e. TopSp <-> D e. ( *Met ` X ) ) )
34 33 pm5.32ri 
 |-  ( ( K e. TopSp /\ J = ( MetOpen ` D ) ) <-> ( D e. ( *Met ` X ) /\ J = ( MetOpen ` D ) ) )
35 4 34 bitri 
 |-  ( K e. *MetSp <-> ( D e. ( *Met ` X ) /\ J = ( MetOpen ` D ) ) )