Metamath Proof Explorer


Theorem funcnvpr

Description: The converse pair of ordered pairs is a function if the second members are different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021)

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

Proof

Step Hyp Ref Expression
1 funcnvsn
 |-  Fun `' { <. A , B >. }
2 funcnvsn
 |-  Fun `' { <. C , D >. }
3 1 2 pm3.2i
 |-  ( Fun `' { <. A , B >. } /\ Fun `' { <. C , D >. } )
4 df-rn
 |-  ran { <. A , B >. } = dom `' { <. A , B >. }
5 rnsnopg
 |-  ( A e. U -> ran { <. A , B >. } = { B } )
6 4 5 eqtr3id
 |-  ( A e. U -> dom `' { <. A , B >. } = { B } )
7 df-rn
 |-  ran { <. C , D >. } = dom `' { <. C , D >. }
8 rnsnopg
 |-  ( C e. V -> ran { <. C , D >. } = { D } )
9 7 8 eqtr3id
 |-  ( C e. V -> dom `' { <. C , D >. } = { D } )
10 6 9 ineqan12d
 |-  ( ( A e. U /\ C e. V ) -> ( dom `' { <. A , B >. } i^i dom `' { <. C , D >. } ) = ( { B } i^i { D } ) )
11 10 3adant3
 |-  ( ( A e. U /\ C e. V /\ B =/= D ) -> ( dom `' { <. A , B >. } i^i dom `' { <. C , D >. } ) = ( { B } i^i { D } ) )
12 disjsn2
 |-  ( B =/= D -> ( { B } i^i { D } ) = (/) )
13 12 3ad2ant3
 |-  ( ( A e. U /\ C e. V /\ B =/= D ) -> ( { B } i^i { D } ) = (/) )
14 11 13 eqtrd
 |-  ( ( A e. U /\ C e. V /\ B =/= D ) -> ( dom `' { <. A , B >. } i^i dom `' { <. C , D >. } ) = (/) )
15 funun
 |-  ( ( ( Fun `' { <. A , B >. } /\ Fun `' { <. C , D >. } ) /\ ( dom `' { <. A , B >. } i^i dom `' { <. C , D >. } ) = (/) ) -> Fun ( `' { <. A , B >. } u. `' { <. C , D >. } ) )
16 3 14 15 sylancr
 |-  ( ( A e. U /\ C e. V /\ B =/= D ) -> Fun ( `' { <. A , B >. } u. `' { <. C , D >. } ) )
17 df-pr
 |-  { <. A , B >. , <. C , D >. } = ( { <. A , B >. } u. { <. C , D >. } )
18 17 cnveqi
 |-  `' { <. A , B >. , <. C , D >. } = `' ( { <. A , B >. } u. { <. C , D >. } )
19 cnvun
 |-  `' ( { <. A , B >. } u. { <. C , D >. } ) = ( `' { <. A , B >. } u. `' { <. C , D >. } )
20 18 19 eqtri
 |-  `' { <. A , B >. , <. C , D >. } = ( `' { <. A , B >. } u. `' { <. C , D >. } )
21 20 funeqi
 |-  ( Fun `' { <. A , B >. , <. C , D >. } <-> Fun ( `' { <. A , B >. } u. `' { <. C , D >. } ) )
22 16 21 sylibr
 |-  ( ( A e. U /\ C e. V /\ B =/= D ) -> Fun `' { <. A , B >. , <. C , D >. } )