Metamath Proof Explorer

Theorem funcnvqp

Description: The converse quadruple 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) (Proof shortened by JJ, 14-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 funcnvpr 
 |-  ( ( A e. U /\ C e. V /\ B =/= D ) -> Fun `' { <. A , B >. , <. C , D >. } )
2 1 3expa 
 |-  ( ( ( A e. U /\ C e. V ) /\ B =/= D ) -> Fun `' { <. A , B >. , <. C , D >. } )
3 2 3ad2antr1 
 |-  ( ( ( A e. U /\ C e. V ) /\ ( B =/= D /\ B =/= F /\ B =/= H ) ) -> Fun `' { <. A , B >. , <. C , D >. } )
4 3 ad2ant2r 
 |-  ( ( ( ( A e. U /\ C e. V ) /\ ( E e. W /\ G e. T ) ) /\ ( ( B =/= D /\ B =/= F /\ B =/= H ) /\ F =/= H ) ) -> Fun `' { <. A , B >. , <. C , D >. } )
5 4 3adantr2 
 |-  ( ( ( ( A e. U /\ C e. V ) /\ ( E e. W /\ G e. T ) ) /\ ( ( B =/= D /\ B =/= F /\ B =/= H ) /\ ( D =/= F /\ D =/= H ) /\ F =/= H ) ) -> Fun `' { <. A , B >. , <. C , D >. } )
6 funcnvpr 
 |-  ( ( E e. W /\ G e. T /\ F =/= H ) -> Fun `' { <. E , F >. , <. G , H >. } )
7 6 3expa 
 |-  ( ( ( E e. W /\ G e. T ) /\ F =/= H ) -> Fun `' { <. E , F >. , <. G , H >. } )
8 7 ad2ant2l 
 |-  ( ( ( ( A e. U /\ C e. V ) /\ ( E e. W /\ G e. T ) ) /\ ( ( B =/= D /\ B =/= F /\ B =/= H ) /\ F =/= H ) ) -> Fun `' { <. E , F >. , <. G , H >. } )
9 8 3adantr2 
 |-  ( ( ( ( A e. U /\ C e. V ) /\ ( E e. W /\ G e. T ) ) /\ ( ( B =/= D /\ B =/= F /\ B =/= H ) /\ ( D =/= F /\ D =/= H ) /\ F =/= H ) ) -> Fun `' { <. E , F >. , <. G , H >. } )
10 df-rn 
 |-  ran { <. A , B >. , <. C , D >. } = dom `' { <. A , B >. , <. C , D >. }
11 rnpropg 
 |-  ( ( A e. U /\ C e. V ) -> ran { <. A , B >. , <. C , D >. } = { B , D } )
12 10 11 syl5eqr 
 |-  ( ( A e. U /\ C e. V ) -> dom `' { <. A , B >. , <. C , D >. } = { B , D } )
13 df-rn 
 |-  ran { <. E , F >. , <. G , H >. } = dom `' { <. E , F >. , <. G , H >. }
14 rnpropg 
 |-  ( ( E e. W /\ G e. T ) -> ran { <. E , F >. , <. G , H >. } = { F , H } )
15 13 14 syl5eqr 
 |-  ( ( E e. W /\ G e. T ) -> dom `' { <. E , F >. , <. G , H >. } = { F , H } )
16 12 15 ineqan12d 
 |-  ( ( ( A e. U /\ C e. V ) /\ ( E e. W /\ G e. T ) ) -> ( dom `' { <. A , B >. , <. C , D >. } i^i dom `' { <. E , F >. , <. G , H >. } ) = ( { B , D } i^i { F , H } ) )
17 disjpr2 
 |-  ( ( ( B =/= F /\ D =/= F ) /\ ( B =/= H /\ D =/= H ) ) -> ( { B , D } i^i { F , H } ) = (/) )
18 17 an4s 
 |-  ( ( ( B =/= F /\ B =/= H ) /\ ( D =/= F /\ D =/= H ) ) -> ( { B , D } i^i { F , H } ) = (/) )
19 18 3adantl1 
 |-  ( ( ( B =/= D /\ B =/= F /\ B =/= H ) /\ ( D =/= F /\ D =/= H ) ) -> ( { B , D } i^i { F , H } ) = (/) )
20 19 3adant3 
 |-  ( ( ( B =/= D /\ B =/= F /\ B =/= H ) /\ ( D =/= F /\ D =/= H ) /\ F =/= H ) -> ( { B , D } i^i { F , H } ) = (/) )
21 16 20 sylan9eq 
 |-  ( ( ( ( A e. U /\ C e. V ) /\ ( E e. W /\ G e. T ) ) /\ ( ( B =/= D /\ B =/= F /\ B =/= H ) /\ ( D =/= F /\ D =/= H ) /\ F =/= H ) ) -> ( dom `' { <. A , B >. , <. C , D >. } i^i dom `' { <. E , F >. , <. G , H >. } ) = (/) )
22 funun 
 |-  ( ( ( Fun `' { <. A , B >. , <. C , D >. } /\ Fun `' { <. E , F >. , <. G , H >. } ) /\ ( dom `' { <. A , B >. , <. C , D >. } i^i dom `' { <. E , F >. , <. G , H >. } ) = (/) ) -> Fun ( `' { <. A , B >. , <. C , D >. } u. `' { <. E , F >. , <. G , H >. } ) )
23 5 9 21 22 syl21anc 
 |-  ( ( ( ( A e. U /\ C e. V ) /\ ( E e. W /\ G e. T ) ) /\ ( ( B =/= D /\ B =/= F /\ B =/= H ) /\ ( D =/= F /\ D =/= H ) /\ F =/= H ) ) -> Fun ( `' { <. A , B >. , <. C , D >. } u. `' { <. E , F >. , <. G , H >. } ) )
24 cnvun 
 |-  `' ( { <. A , B >. , <. C , D >. } u. { <. E , F >. , <. G , H >. } ) = ( `' { <. A , B >. , <. C , D >. } u. `' { <. E , F >. , <. G , H >. } )
25 24 funeqi 
 |-  ( Fun `' ( { <. A , B >. , <. C , D >. } u. { <. E , F >. , <. G , H >. } ) <-> Fun ( `' { <. A , B >. , <. C , D >. } u. `' { <. E , F >. , <. G , H >. } ) )
26 23 25 sylibr 
 |-  ( ( ( ( A e. U /\ C e. V ) /\ ( E e. W /\ G e. T ) ) /\ ( ( B =/= D /\ B =/= F /\ B =/= H ) /\ ( D =/= F /\ D =/= H ) /\ F =/= H ) ) -> Fun `' ( { <. A , B >. , <. C , D >. } u. { <. E , F >. , <. G , H >. } ) )