Metamath Proof Explorer

Theorem cnvprop

Description: Converse of a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Assertion cnvprop 
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. V /\ D e. W ) ) -> `' { <. A , B >. , <. C , D >. } = { <. B , A >. , <. D , C >. } )

Proof

Step Hyp Ref Expression
1 cnvsng 
 |-  ( ( A e. V /\ B e. W ) -> `' { <. A , B >. } = { <. B , A >. } )
2 1 adantr 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. V /\ D e. W ) ) -> `' { <. A , B >. } = { <. B , A >. } )
3 cnvsng 
 |-  ( ( C e. V /\ D e. W ) -> `' { <. C , D >. } = { <. D , C >. } )
4 3 adantl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. V /\ D e. W ) ) -> `' { <. C , D >. } = { <. D , C >. } )
5 2 4 uneq12d 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. V /\ D e. W ) ) -> ( `' { <. A , B >. } u. `' { <. C , D >. } ) = ( { <. B , A >. } u. { <. D , C >. } ) )
6 df-pr 
 |-  { <. A , B >. , <. C , D >. } = ( { <. A , B >. } u. { <. C , D >. } )
7 6 cnveqi 
 |-  `' { <. A , B >. , <. C , D >. } = `' ( { <. A , B >. } u. { <. C , D >. } )
8 cnvun 
 |-  `' ( { <. A , B >. } u. { <. C , D >. } ) = ( `' { <. A , B >. } u. `' { <. C , D >. } )
9 7 8 eqtri 
 |-  `' { <. A , B >. , <. C , D >. } = ( `' { <. A , B >. } u. `' { <. C , D >. } )
10 df-pr 
 |-  { <. B , A >. , <. D , C >. } = ( { <. B , A >. } u. { <. D , C >. } )
11 5 9 10 3eqtr4g 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. V /\ D e. W ) ) -> `' { <. A , B >. , <. C , D >. } = { <. B , A >. , <. D , C >. } )