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 = { 𝑓 ∈ TopSp ∣ ( TopOpen ‘ 𝑓 ) = ( MetOpen ‘ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxms ⊢ ∞MetSp
1 vf ⊢ 𝑓
2 ctps ⊢ TopSp
3 ctopn ⊢ TopOpen
4 1 cv ⊢ 𝑓
5 4 3 cfv ⊢ ( TopOpen ‘ 𝑓 )
6 cmopn ⊢ MetOpen
7 cds ⊢ dist
8 4 7 cfv ⊢ ( dist ‘ 𝑓 )
9 cbs ⊢ Base
10 4 9 cfv ⊢ ( Base ‘ 𝑓 )
11 10 10 cxp ⊢ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) )
12 8 11 cres ⊢ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) )
13 12 6 cfv ⊢ ( MetOpen ‘ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) )
14 5 13 wceq ⊢ ( TopOpen ‘ 𝑓 ) = ( MetOpen ‘ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) )
15 14 1 2 crab ⊢ { 𝑓 ∈ TopSp ∣ ( TopOpen ‘ 𝑓 ) = ( MetOpen ‘ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) ) }
16 0 15 wceq ⊢ ∞MetSp = { 𝑓 ∈ TopSp ∣ ( TopOpen ‘ 𝑓 ) = ( MetOpen ‘ ( ( dist ‘ 𝑓 ) ↾ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) ) }