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 simpr 
 |-  ( ( ph /\ D e. U. ran *Met ) -> D e. U. ran *Met )
10 xmetunirn 
 |-  ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )
11 9 10 sylib 
 |-  ( ( ph /\ D e. U. ran *Met ) -> D e. ( *Met ` dom dom D ) )
12 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
13 12 mopnuni 
 |-  ( D e. ( *Met ` dom dom D ) -> dom dom D = U. ( MetOpen ` D ) )
14 11 13 syl 
 |-  ( ( ph /\ D e. U. ran *Met ) -> dom dom D = U. ( MetOpen ` D ) )
15 2 dmeqd 
 |-  ( ph -> dom D = dom ( ( dist ` M ) |` ( X X. X ) ) )
16 dmres 
 |-  dom ( ( dist ` M ) |` ( X X. X ) ) = ( ( X X. X ) i^i dom ( dist ` M ) )
17 15 16 eqtrdi 
 |-  ( ph -> dom D = ( ( X X. X ) i^i dom ( dist ` M ) ) )
18 inss1 
 |-  ( ( X X. X ) i^i dom ( dist ` M ) ) C_ ( X X. X )
19 17 18 eqsstrdi 
 |-  ( ph -> dom D C_ ( X X. X ) )
20 dmss 
 |-  ( dom D C_ ( X X. X ) -> dom dom D C_ dom ( X X. X ) )
21 19 20 syl 
 |-  ( ph -> dom dom D C_ dom ( X X. X ) )
22 dmxpid 
 |-  dom ( X X. X ) = X
23 21 22 sseqtrdi 
 |-  ( ph -> dom dom D C_ X )
24 23 adantr 
 |-  ( ( ph /\ D e. U. ran *Met ) -> dom dom D C_ X )
25 14 24 eqsstrrd 
 |-  ( ( ph /\ D e. U. ran *Met ) -> U. ( MetOpen ` D ) C_ X )
26 sspwuni 
 |-  ( ( MetOpen ` D ) C_ ~P X <-> U. ( MetOpen ` D ) C_ X )
27 25 26 sylibr 
 |-  ( ( ph /\ D e. U. ran *Met ) -> ( MetOpen ` D ) C_ ~P X )
28 27 ex 
 |-  ( ph -> ( D e. U. ran *Met -> ( MetOpen ` D ) C_ ~P X ) )
29 8 28 syl5 
 |-  ( ph -> ( D e. dom MetOpen -> ( MetOpen ` D ) C_ ~P X ) )
30 ndmfv 
 |-  ( -. D e. dom MetOpen -> ( MetOpen ` D ) = (/) )
31 0ss 
 |-  (/) C_ ~P X
32 30 31 eqsstrdi 
 |-  ( -. D e. dom MetOpen -> ( MetOpen ` D ) C_ ~P X )
33 29 32 pm2.61d1 
 |-  ( ph -> ( MetOpen ` D ) C_ ~P X )
34 1 2 3 setsmsbas 
 |-  ( ph -> X = ( Base ` K ) )
35 34 pweqd 
 |-  ( ph -> ~P X = ~P ( Base ` K ) )
36 33 5 35 3sstr3d 
 |-  ( ph -> ( TopSet ` K ) C_ ~P ( Base ` K ) )
37 eqid 
 |-  ( Base ` K ) = ( Base ` K )
38 eqid 
 |-  ( TopSet ` K ) = ( TopSet ` K )
39 37 38 topnid 
 |-  ( ( TopSet ` K ) C_ ~P ( Base ` K ) -> ( TopSet ` K ) = ( TopOpen ` K ) )
40 36 39 syl 
 |-  ( ph -> ( TopSet ` K ) = ( TopOpen ` K ) )
41 5 40 eqtrd 
 |-  ( ph -> ( MetOpen ` D ) = ( TopOpen ` K ) )