Metamath Proof Explorer

Theorem xmettpos

Description: The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmettpos 
|- ( D e. ( *Met ` X ) -> tpos D = D )

Proof

Step Hyp Ref Expression
1 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ y e. X ) -> ( x D y ) = ( y D x ) )
2 1 3expb 
 |-  ( ( D e. ( *Met ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x D y ) = ( y D x ) )
3 2 ralrimivva 
 |-  ( D e. ( *Met ` X ) -> A. x e. X A. y e. X ( x D y ) = ( y D x ) )
4 xmetf 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
5 ffn 
 |-  ( D : ( X X. X ) --> RR* -> D Fn ( X X. X ) )
6 tpossym 
 |-  ( D Fn ( X X. X ) -> ( tpos D = D <-> A. x e. X A. y e. X ( x D y ) = ( y D x ) ) )
7 4 5 6 3syl 
 |-  ( D e. ( *Met ` X ) -> ( tpos D = D <-> A. x e. X A. y e. X ( x D y ) = ( y D x ) ) )
8 3 7 mpbird 
 |-  ( D e. ( *Met ` X ) -> tpos D = D )