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

Metamath Proof Explorer

Definition df-xms

Description: Define the (proper) class of extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion df-xms ⊢ ∞MetSp = f ∈ TopSp | TopOpen ⁡ f = MetOpen ⁡ dist ⁡ f ↾ Base f × Base f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxms class ∞MetSp
1 vf setvar f
2 ctps class TopSp
3 ctopn class TopOpen
4 1 cv setvar f
5 4 3 cfv class TopOpen ⁡ f
6 cmopn class MetOpen
7 cds class dist
8 4 7 cfv class dist ⁡ f
9 cbs class Base
10 4 9 cfv class Base f
11 10 10 cxp class Base f × Base f
12 8 11 cres class dist ⁡ f ↾ Base f × Base f
13 12 6 cfv class MetOpen ⁡ dist ⁡ f ↾ Base f × Base f
14 5 13 wceq wff TopOpen ⁡ f = MetOpen ⁡ dist ⁡ f ↾ Base f × Base f
15 14 1 2 crab class f ∈ TopSp | TopOpen ⁡ f = MetOpen ⁡ dist ⁡ f ↾ Base f × Base f
16 0 15 wceq wff ∞MetSp = f ∈ TopSp | TopOpen ⁡ f = MetOpen ⁡ dist ⁡ f ↾ Base f × Base f