Metamath Proof Explorer

Theorem setsmstopn

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

Ref Expression
Hypotheses setsms.x 
|- ( ph -> X = ( Base ` M ) )
setsms.d 
|- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )
setsms.k 
|- ( ph -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
setsms.m 
|- ( ph -> M e. V )
Assertion setsmstopn 
|- ( ph -> ( MetOpen ` D ) = ( TopOpen ` K ) )

Proof

Step Hyp Ref Expression
1 setsms.x 
 |-  ( ph -> X = ( Base ` M ) )
2 setsms.d 
 |-  ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )
3 setsms.k 
 |-  ( ph -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
4 setsms.m 
 |-  ( ph -> M e. V )
5 1 2 3 4 setsmstset 
 |-  ( ph -> ( MetOpen ` D ) = ( TopSet ` K ) )
6 df-mopn 
 |-  MetOpen = ( x e. U. ran *Met |-> ( topGen ` ran ( ball ` x ) ) )
7 6 dmmptss 
 |-  dom MetOpen C_ U. ran *Met
8 7 sseli 
 |-  ( D e. dom MetOpen -> D e. U. ran *Met )
9 xmetunirn 
 |-  ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )
10 9 bilani 
 |-  ( ( ph /\ D e. U. ran *Met ) -> D e. ( *Met ` dom dom D ) )
11 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
12 11 mopnuni 
 |-  ( D e. ( *Met ` dom dom D ) -> dom dom D = U. ( MetOpen ` D ) )
13 10 12 syl 
 |-  ( ( ph /\ D e. U. ran *Met ) -> dom dom D = U. ( MetOpen ` D ) )
14 2 dmeqd 
 |-  ( ph -> dom D = dom ( ( dist ` M ) |` ( X X. X ) ) )
15 dmres 
 |-  dom ( ( dist ` M ) |` ( X X. X ) ) = ( ( X X. X ) i^i dom ( dist ` M ) )
16 14 15 eqtrdi 
 |-  ( ph -> dom D = ( ( X X. X ) i^i dom ( dist ` M ) ) )
17 inss1 
 |-  ( ( X X. X ) i^i dom ( dist ` M ) ) C_ ( X X. X )
18 16 17 eqsstrdi 
 |-  ( ph -> dom D C_ ( X X. X ) )
19 dmss 
 |-  ( dom D C_ ( X X. X ) -> dom dom D C_ dom ( X X. X ) )
20 18 19 syl 
 |-  ( ph -> dom dom D C_ dom ( X X. X ) )
21 dmxpid 
 |-  dom ( X X. X ) = X
22 20 21 sseqtrdi 
 |-  ( ph -> dom dom D C_ X )
23 22 adantr 
 |-  ( ( ph /\ D e. U. ran *Met ) -> dom dom D C_ X )
24 13 23 eqsstrrd 
 |-  ( ( ph /\ D e. U. ran *Met ) -> U. ( MetOpen ` D ) C_ X )
25 sspwuni 
 |-  ( ( MetOpen ` D ) C_ ~P X <-> U. ( MetOpen ` D ) C_ X )
26 24 25 sylibr 
 |-  ( ( ph /\ D e. U. ran *Met ) -> ( MetOpen ` D ) C_ ~P X )
27 26 ex 
 |-  ( ph -> ( D e. U. ran *Met -> ( MetOpen ` D ) C_ ~P X ) )
28 8 27 syl5 
 |-  ( ph -> ( D e. dom MetOpen -> ( MetOpen ` D ) C_ ~P X ) )
29 ndmfv 
 |-  ( -. D e. dom MetOpen -> ( MetOpen ` D ) = (/) )
30 0ss 
 |-  (/) C_ ~P X
31 29 30 eqsstrdi 
 |-  ( -. D e. dom MetOpen -> ( MetOpen ` D ) C_ ~P X )
32 28 31 pm2.61d1 
 |-  ( ph -> ( MetOpen ` D ) C_ ~P X )
33 1 2 3 setsmsbas 
 |-  ( ph -> X = ( Base ` K ) )
34 33 pweqd 
 |-  ( ph -> ~P X = ~P ( Base ` K ) )
35 32 5 34 3sstr3d 
 |-  ( ph -> ( TopSet ` K ) C_ ~P ( Base ` K ) )
36 eqid 
 |-  ( Base ` K ) = ( Base ` K )
37 eqid 
 |-  ( TopSet ` K ) = ( TopSet ` K )
38 36 37 topnid 
 |-  ( ( TopSet ` K ) C_ ~P ( Base ` K ) -> ( TopSet ` K ) = ( TopOpen ` K ) )
39 35 38 syl 
 |-  ( ph -> ( TopSet ` K ) = ( TopOpen ` K ) )
40 5 39 eqtrd 
 |-  ( ph -> ( MetOpen ` D ) = ( TopOpen ` K ) )