Metamath Proof Explorer

Theorem isxms

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}=\mathrm{TopOpen}\left({K}\right)$
isms.x ${⊢}{X}={\mathrm{Base}}_{{K}}$
isms.d ${⊢}{D}={\mathrm{dist}\left({K}\right)↾}_{\left({X}×{X}\right)}$
Assertion isxms ${⊢}{K}\in \mathrm{\infty MetSp}↔\left({K}\in \mathrm{TopSp}\wedge {J}=\mathrm{MetOpen}\left({D}\right)\right)$

Proof

Step Hyp Ref Expression
1 isms.j ${⊢}{J}=\mathrm{TopOpen}\left({K}\right)$
2 isms.x ${⊢}{X}={\mathrm{Base}}_{{K}}$
3 isms.d ${⊢}{D}={\mathrm{dist}\left({K}\right)↾}_{\left({X}×{X}\right)}$
4 fveq2 ${⊢}{f}={K}\to \mathrm{TopOpen}\left({f}\right)=\mathrm{TopOpen}\left({K}\right)$
5 4 1 eqtr4di ${⊢}{f}={K}\to \mathrm{TopOpen}\left({f}\right)={J}$
6 fveq2 ${⊢}{f}={K}\to \mathrm{dist}\left({f}\right)=\mathrm{dist}\left({K}\right)$
7 fveq2 ${⊢}{f}={K}\to {\mathrm{Base}}_{{f}}={\mathrm{Base}}_{{K}}$
8 7 2 eqtr4di ${⊢}{f}={K}\to {\mathrm{Base}}_{{f}}={X}$
9 8 sqxpeqd ${⊢}{f}={K}\to {\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}={X}×{X}$
10 6 9 reseq12d ${⊢}{f}={K}\to {\mathrm{dist}\left({f}\right)↾}_{\left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right)}={\mathrm{dist}\left({K}\right)↾}_{\left({X}×{X}\right)}$
11 10 3 eqtr4di ${⊢}{f}={K}\to {\mathrm{dist}\left({f}\right)↾}_{\left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right)}={D}$
12 11 fveq2d ${⊢}{f}={K}\to \mathrm{MetOpen}\left({\mathrm{dist}\left({f}\right)↾}_{\left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right)}\right)=\mathrm{MetOpen}\left({D}\right)$
13 5 12 eqeq12d ${⊢}{f}={K}\to \left(\mathrm{TopOpen}\left({f}\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left({f}\right)↾}_{\left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right)}\right)↔{J}=\mathrm{MetOpen}\left({D}\right)\right)$
14 df-xms ${⊢}\mathrm{\infty MetSp}=\left\{{f}\in \mathrm{TopSp}|\mathrm{TopOpen}\left({f}\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left({f}\right)↾}_{\left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right)}\right)\right\}$
15 13 14 elrab2 ${⊢}{K}\in \mathrm{\infty MetSp}↔\left({K}\in \mathrm{TopSp}\wedge {J}=\mathrm{MetOpen}\left({D}\right)\right)$