Metamath Proof Explorer

Definition df-psmet

Description: Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018)

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

Detailed syntax breakdown

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