Definition df-xmet

Description: Define the set of all extended metrics on a given base set. The definition is similar to df-met , but we also allow the metric to take on the value +oo . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	df-xmet	|- *Met = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxmet	|- *Met
1		vx	|- x
2		cvv	|- _V
3		vd	|- d
4		cxr	|- RR*
5		cmap	|- ^m
6	1	cv	|- x
7	6 6	cxp	|- ( x X. x )
8	4 7 5	co	|- ( RR* ^m ( x X. x ) )
9		vy	|- y
10		vz	|- z
11	9	cv	|- y
12	3	cv	|- d
13	10	cv	|- z
14	11 13 12	co	|- ( y d z )
15		cc0	|- 0
16	14 15	wceq	|- ( y d z ) = 0
17	11 13	wceq	|- y = z
18	16 17	wb	|- ( ( y d z ) = 0 <-> y = z )
19		vw	|- w
20		cle	|- <_
21	19	cv	|- w
22	21 11 12	co	|- ( w d y )
23		cxad	|- +e
24	21 13 12	co	|- ( w d z )
25	22 24 23	co	|- ( ( w d y ) +e ( w d z ) )
26	14 25 20	wbr	|- ( y d z ) <_ ( ( w d y ) +e ( w d z ) )
27	26 19 6	wral	|- A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) )
28	18 27	wa	|- ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) )
29	28 10 6	wral	|- A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) )
30	29 9 6	wral	|- A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) )
31	30 3 8	crab	|- { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) }
32	1 2 31	cmpt	|- ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
33	0 32	wceq	|- *Met = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )