This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = TopOpen ⁡ K
isms.x ⊢ X = Base K
isms.d ⊢ D = dist ⁡ K ↾ X × X
Assertion isxms ⊢ K ∈ ∞MetSp ↔ K ∈ TopSp ∧ 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
4 fveq2 ⊢ f = K → TopOpen ⁡ f = TopOpen ⁡ K
5 4 1 eqtr4di ⊢ f = K → TopOpen ⁡ f = J
6 fveq2 ⊢ f = K → dist ⁡ f = dist ⁡ K
7 fveq2 ⊢ f = K → Base f = Base K
8 7 2 eqtr4di ⊢ f = K → Base f = X
9 8 sqxpeqd ⊢ f = K → Base f × Base f = X × X
10 6 9 reseq12d ⊢ f = K → dist ⁡ f ↾ Base f × Base f = dist ⁡ K ↾ X × X
11 10 3 eqtr4di ⊢ f = K → dist ⁡ f ↾ Base f × Base f = D
12 11 fveq2d ⊢ f = K → MetOpen ⁡ dist ⁡ f ↾ Base f × Base f = MetOpen ⁡ D
13 5 12 eqeq12d ⊢ f = K → TopOpen ⁡ f = MetOpen ⁡ dist ⁡ f ↾ Base f × Base f ↔ J = MetOpen ⁡ D
14 df-xms ⊢ ∞MetSp = f ∈ TopSp | TopOpen ⁡ f = MetOpen ⁡ dist ⁡ f ↾ Base f × Base f
15 13 14 elrab2 ⊢ K ∈ ∞MetSp ↔ K ∈ TopSp ∧ J = MetOpen ⁡ D