Definition df-metid 29931

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

Assertion

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

Distinct variable group:   x, d, y

Detailed syntax breakdown of Definition df-metid

Step	Hyp	Ref	Expression
1		cmetid 29929	. 2 class ~Met
2		vd	. . 3 setvar d
3		cpsmet 19730	. . . . 5 class PsMet
4	3	crn 5115	. . . 4 class ran PsMet
5	4	cuni 4436	. . 3 class U. ran PsMet
6		vx	. . . . . . . 8 setvar x
7	6	cv 1482	. . . . . . 7 class x
8	2	cv 1482	. . . . . . . . 9 class d
9	8	cdm 5114	. . . . . . . 8 class dom d
10	9	cdm 5114	. . . . . . 7 class dom dom d
11	7, 10	wcel 1990	. . . . . 6 wff x e. dom dom d
12		vy	. . . . . . . 8 setvar y
13	12	cv 1482	. . . . . . 7 class y
14	13, 10	wcel 1990	. . . . . 6 wff y e. dom dom d
15	11, 14	wa 384	. . . . 5 wff ( x e. dom dom d /\ y e. dom dom d )
16	7, 13, 8	co 6650	. . . . . 6 class ( x d y )
17		cc0 9936	. . . . . 6 class 0
18	16, 17	wceq 1483	. . . . 5 wff ( x d y ) = 0
19	15, 18	wa 384	. . . 4 wff ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 )
20	19, 6, 12	copab 4712	. . 3 class { <. x , y >. | ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 ) }
21	2, 5, 20	cmpt 4729	. 2 class ( d e. U. ran PsMet |-> { <. x , y >. | ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 ) } )
22	1, 21	wceq 1483	1 wff ~Met = ( d e. U. ran PsMet |-> { <. x , y >. | ( ( x e. dom dom d /\ y e. dom dom d ) /\ ( x d y ) = 0 ) } )

This definition is referenced by:  metidval  29933