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=TopOpenK
isms.x X=BaseK
isms.d D=distKX×X
Assertion isxms2 K∞MetSpD∞MetXJ=MetOpenD

Proof

Step Hyp Ref Expression
1 isms.j J=TopOpenK
2 isms.x X=BaseK
3 isms.d D=distKX×X
4 1 2 3 isxms K∞MetSpKTopSpJ=MetOpenD
5 2 1 istps KTopSpJTopOnX
6 df-mopn MetOpen=xran∞MettopGenranballx
7 6 dmmptss domMetOpenran∞Met
8 toponmax JTopOnXXJ
9 8 adantl J=MetOpenDJTopOnXXJ
10 simpl J=MetOpenDJTopOnXJ=MetOpenD
11 9 10 eleqtrd J=MetOpenDJTopOnXXMetOpenD
12 elfvdm XMetOpenDDdomMetOpen
13 11 12 syl J=MetOpenDJTopOnXDdomMetOpen
14 7 13 sselid J=MetOpenDJTopOnXDran∞Met
15 xmetunirn Dran∞MetD∞MetdomdomD
16 14 15 sylib J=MetOpenDJTopOnXD∞MetdomdomD
17 eqid MetOpenD=MetOpenD
18 17 mopntopon D∞MetdomdomDMetOpenDTopOndomdomD
19 16 18 syl J=MetOpenDJTopOnXMetOpenDTopOndomdomD
20 10 19 eqeltrd J=MetOpenDJTopOnXJTopOndomdomD
21 toponuni JTopOndomdomDdomdomD=J
22 20 21 syl J=MetOpenDJTopOnXdomdomD=J
23 toponuni JTopOnXX=J
24 23 adantl J=MetOpenDJTopOnXX=J
25 22 24 eqtr4d J=MetOpenDJTopOnXdomdomD=X
26 25 fveq2d J=MetOpenDJTopOnX∞MetdomdomD=∞MetX
27 16 26 eleqtrd J=MetOpenDJTopOnXD∞MetX
28 27 ex J=MetOpenDJTopOnXD∞MetX
29 17 mopntopon D∞MetXMetOpenDTopOnX
30 eleq1 J=MetOpenDJTopOnXMetOpenDTopOnX
31 29 30 syl5ibr J=MetOpenDD∞MetXJTopOnX
32 28 31 impbid J=MetOpenDJTopOnXD∞MetX
33 5 32 syl5bb J=MetOpenDKTopSpD∞MetX
34 33 pm5.32ri KTopSpJ=MetOpenDD∞MetXJ=MetOpenD
35 4 34 bitri K∞MetSpD∞MetXJ=MetOpenD