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 ‘ 𝑓 ) ) ) ) }