Definition df-metid

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

	Ref	Expression
Assertion	df-metid	|- ~Met = ( d e. U. ran PsMet |-> { <. x , y >. | ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmetid	|- ~Met
1		vd	|- d
2		cpsmet	|- PsMet
3	2	crn	|- ran PsMet
4	3	cuni	|- U. ran PsMet
5		vx	|- x
6		vy	|- y
7	5	cv	|- x
8	1	cv	|- d
9	8	cdm	|- dom d
10	9	cdm	|- dom dom d
11	7 10	wcel	|- x e. dom dom d
12	6	cv	|- y
13	12 10	wcel	|- y e. dom dom d
14	11 13	wa	|- ( x e. dom dom d /\ y e. dom dom d )
15	7 12 8	co	|- ( x d y )
16		cc0	|- 0
17	15 16	wceq	|- ( x d y ) = 0
18	14 17	wa	|- ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 )
19	18 5 6	copab	|- { <. x , y >. | ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 ) }
20	1 4 19	cmpt	|- ( d e. U. ran PsMet |-> { <. x , y >. | ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 ) } )
21	0 20	wceq	|- ~Met = ( d e. U. ran PsMet |-> { <. x , y >. | ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 ) } )