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 >. } )