Metamath Proof Explorer

Theorem funcnvtp

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

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. U /\ C e. V /\ E e. W ) -> A e. U )
2 simp2 
 |-  ( ( A e. U /\ C e. V /\ E e. W ) -> C e. V )
3 simp1 
 |-  ( ( B =/= D /\ B =/= F /\ D =/= F ) -> B =/= D )
4 funcnvpr 
 |-  ( ( A e. U /\ C e. V /\ B =/= D ) -> Fun `' { <. A , B >. , <. C , D >. } )
5 1 2 3 4 syl2an3an 
 |-  ( ( ( A e. U /\ C e. V /\ E e. W ) /\ ( B =/= D /\ B =/= F /\ D =/= F ) ) -> Fun `' { <. A , B >. , <. C , D >. } )
6 funcnvsn 
 |-  Fun `' { <. E , F >. }
7 6 a1i 
 |-  ( ( ( A e. U /\ C e. V /\ E e. W ) /\ ( B =/= D /\ B =/= F /\ D =/= F ) ) -> Fun `' { <. E , F >. } )
8 df-rn 
 |-  ran { <. A , B >. , <. C , D >. } = dom `' { <. A , B >. , <. C , D >. }
9 rnpropg 
 |-  ( ( A e. U /\ C e. V ) -> ran { <. A , B >. , <. C , D >. } = { B , D } )
10 8 9 eqtr3id 
 |-  ( ( A e. U /\ C e. V ) -> dom `' { <. A , B >. , <. C , D >. } = { B , D } )
11 10 3adant3 
 |-  ( ( A e. U /\ C e. V /\ E e. W ) -> dom `' { <. A , B >. , <. C , D >. } = { B , D } )
12 df-rn 
 |-  ran { <. E , F >. } = dom `' { <. E , F >. }
13 rnsnopg 
 |-  ( E e. W -> ran { <. E , F >. } = { F } )
14 12 13 eqtr3id 
 |-  ( E e. W -> dom `' { <. E , F >. } = { F } )
15 14 3ad2ant3 
 |-  ( ( A e. U /\ C e. V /\ E e. W ) -> dom `' { <. E , F >. } = { F } )
16 11 15 ineq12d 
 |-  ( ( A e. U /\ C e. V /\ E e. W ) -> ( dom `' { <. A , B >. , <. C , D >. } i^i dom `' { <. E , F >. } ) = ( { B , D } i^i { F } ) )
17 disjprsn 
 |-  ( ( B =/= F /\ D =/= F ) -> ( { B , D } i^i { F } ) = (/) )
18 17 3adant1 
 |-  ( ( B =/= D /\ B =/= F /\ D =/= F ) -> ( { B , D } i^i { F } ) = (/) )
19 16 18 sylan9eq 
 |-  ( ( ( A e. U /\ C e. V /\ E e. W ) /\ ( B =/= D /\ B =/= F /\ D =/= F ) ) -> ( dom `' { <. A , B >. , <. C , D >. } i^i dom `' { <. E , F >. } ) = (/) )
20 funun 
 |-  ( ( ( Fun `' { <. A , B >. , <. C , D >. } /\ Fun `' { <. E , F >. } ) /\ ( dom `' { <. A , B >. , <. C , D >. } i^i dom `' { <. E , F >. } ) = (/) ) -> Fun ( `' { <. A , B >. , <. C , D >. } u. `' { <. E , F >. } ) )
21 5 7 19 20 syl21anc 
 |-  ( ( ( A e. U /\ C e. V /\ E e. W ) /\ ( B =/= D /\ B =/= F /\ D =/= F ) ) -> Fun ( `' { <. A , B >. , <. C , D >. } u. `' { <. E , F >. } ) )
22 df-tp 
 |-  { <. A , B >. , <. C , D >. , <. E , F >. } = ( { <. A , B >. , <. C , D >. } u. { <. E , F >. } )
23 22 cnveqi 
 |-  `' { <. A , B >. , <. C , D >. , <. E , F >. } = `' ( { <. A , B >. , <. C , D >. } u. { <. E , F >. } )
24 cnvun 
 |-  `' ( { <. A , B >. , <. C , D >. } u. { <. E , F >. } ) = ( `' { <. A , B >. , <. C , D >. } u. `' { <. E , F >. } )
25 23 24 eqtri 
 |-  `' { <. A , B >. , <. C , D >. , <. E , F >. } = ( `' { <. A , B >. , <. C , D >. } u. `' { <. E , F >. } )
26 25 funeqi 
 |-  ( Fun `' { <. A , B >. , <. C , D >. , <. E , F >. } <-> Fun ( `' { <. A , B >. , <. C , D >. } u. `' { <. E , F >. } ) )
27 21 26 sylibr 
 |-  ( ( ( A e. U /\ C e. V /\ E e. W ) /\ ( B =/= D /\ B =/= F /\ D =/= F ) ) -> Fun `' { <. A , B >. , <. C , D >. , <. E , F >. } )