Metamath Proof Explorer

Theorem tpossym

Description: Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion tpossym 
|- ( F Fn ( A X. A ) -> ( tpos F = F <-> A. x e. A A. y e. A ( x F y ) = ( y F x ) ) )

Proof

Step Hyp Ref Expression
1 tposfn 
 |-  ( F Fn ( A X. A ) -> tpos F Fn ( A X. A ) )
2 eqfnov2 
 |-  ( ( tpos F Fn ( A X. A ) /\ F Fn ( A X. A ) ) -> ( tpos F = F <-> A. x e. A A. y e. A ( x tpos F y ) = ( x F y ) ) )
3 1 2 mpancom 
 |-  ( F Fn ( A X. A ) -> ( tpos F = F <-> A. x e. A A. y e. A ( x tpos F y ) = ( x F y ) ) )
4 eqcom 
 |-  ( ( x tpos F y ) = ( x F y ) <-> ( x F y ) = ( x tpos F y ) )
5 ovtpos 
 |-  ( x tpos F y ) = ( y F x )
6 5 eqeq2i 
 |-  ( ( x F y ) = ( x tpos F y ) <-> ( x F y ) = ( y F x ) )
7 4 6 bitri 
 |-  ( ( x tpos F y ) = ( x F y ) <-> ( x F y ) = ( y F x ) )
8 7 2ralbii 
 |-  ( A. x e. A A. y e. A ( x tpos F y ) = ( x F y ) <-> A. x e. A A. y e. A ( x F y ) = ( y F x ) )
9 3 8 bitrdi 
 |-  ( F Fn ( A X. A ) -> ( tpos F = F <-> A. x e. A A. y e. A ( x F y ) = ( y F x ) ) )