Definition df-pstm

Description: Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018)

	Ref	Expression
Assertion	df-pstm	|- pstoMet = ( d e. U. ran PsMet |-> ( a e. ( dom dom d /. ( ~Met ` d ) ) , b e. ( dom dom d /. ( ~Met ` d ) ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpstm	|- pstoMet
1		vd	|- d
2		cpsmet	|- PsMet
3	2	crn	|- ran PsMet
4	3	cuni	|- U. ran PsMet
5		va	|- a
6	1	cv	|- d
7	6	cdm	|- dom d
8	7	cdm	|- dom dom d
9		cmetid	|- ~Met
10	6 9	cfv	|- ( ~Met ` d )
11	8 10	cqs	|- ( dom dom d /. ( ~Met ` d ) )
12		vb	|- b
13		vz	|- z
14		vx	|- x
15	5	cv	|- a
16		vy	|- y
17	12	cv	|- b
18	13	cv	|- z
19	14	cv	|- x
20	16	cv	|- y
21	19 20 6	co	|- ( x d y )
22	18 21	wceq	|- z = ( x d y )
23	22 16 17	wrex	|- E. y e. b z = ( x d y )
24	23 14 15	wrex	|- E. x e. a E. y e. b z = ( x d y )
25	24 13	cab	|- { z | E. x e. a E. y e. b z = ( x d y ) }
26	25	cuni	|- U. { z | E. x e. a E. y e. b z = ( x d y ) }
27	5 12 11 11 26	cmpo	|- ( a e. ( dom dom d /. ( ~Met ` d ) ) , b e. ( dom dom d /. ( ~Met ` d ) ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } )
28	1 4 27	cmpt	|- ( d e. U. ran PsMet |-> ( a e. ( dom dom d /. ( ~Met ` d ) ) , b e. ( dom dom d /. ( ~Met ` d ) ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } ) )
29	0 28	wceq	|- pstoMet = ( d e. U. ran PsMet |-> ( a e. ( dom dom d /. ( ~Met ` d ) ) , b e. ( dom dom d /. ( ~Met ` d ) ) |-> U. { z | E. x e. a E. y e. b z = ( x d y ) } ) )