Metamath Proof Explorer


Theorem relbrtpos

Description: The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 3-Nov-2015)

Ref Expression
Assertion relbrtpos
|- ( Rel F -> ( <. A , B >. tpos F C <-> <. B , A >. F C ) )

Proof

Step Hyp Ref Expression
1 reltpos
 |-  Rel tpos F
2 1 a1i
 |-  ( Rel F -> Rel tpos F )
3 brrelex2
 |-  ( ( Rel tpos F /\ <. A , B >. tpos F C ) -> C e. _V )
4 2 3 sylan
 |-  ( ( Rel F /\ <. A , B >. tpos F C ) -> C e. _V )
5 brrelex2
 |-  ( ( Rel F /\ <. B , A >. F C ) -> C e. _V )
6 brtpos
 |-  ( C e. _V -> ( <. A , B >. tpos F C <-> <. B , A >. F C ) )
7 4 5 6 pm5.21nd
 |-  ( Rel F -> ( <. A , B >. tpos F C <-> <. B , A >. F C ) )