Metamath Proof Explorer

Theorem funprg

Description: A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion funprg 
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> Fun { <. A , C >. , <. B , D >. } )

Proof

Step Hyp Ref Expression
1 funsng 
 |-  ( ( A e. V /\ C e. X ) -> Fun { <. A , C >. } )
2 funsng 
 |-  ( ( B e. W /\ D e. Y ) -> Fun { <. B , D >. } )
3 1 2 anim12i 
 |-  ( ( ( A e. V /\ C e. X ) /\ ( B e. W /\ D e. Y ) ) -> ( Fun { <. A , C >. } /\ Fun { <. B , D >. } ) )
4 3 an4s 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( Fun { <. A , C >. } /\ Fun { <. B , D >. } ) )
5 4 3adant3 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> ( Fun { <. A , C >. } /\ Fun { <. B , D >. } ) )
6 dmsnopg 
 |-  ( C e. X -> dom { <. A , C >. } = { A } )
7 dmsnopg 
 |-  ( D e. Y -> dom { <. B , D >. } = { B } )
8 6 7 ineqan12d 
 |-  ( ( C e. X /\ D e. Y ) -> ( dom { <. A , C >. } i^i dom { <. B , D >. } ) = ( { A } i^i { B } ) )
9 disjsn2 
 |-  ( A =/= B -> ( { A } i^i { B } ) = (/) )
10 8 9 sylan9eq 
 |-  ( ( ( C e. X /\ D e. Y ) /\ A =/= B ) -> ( dom { <. A , C >. } i^i dom { <. B , D >. } ) = (/) )
11 10 3adant1 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> ( dom { <. A , C >. } i^i dom { <. B , D >. } ) = (/) )
12 funun 
 |-  ( ( ( Fun { <. A , C >. } /\ Fun { <. B , D >. } ) /\ ( dom { <. A , C >. } i^i dom { <. B , D >. } ) = (/) ) -> Fun ( { <. A , C >. } u. { <. B , D >. } ) )
13 5 11 12 syl2anc 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> Fun ( { <. A , C >. } u. { <. B , D >. } ) )
14 df-pr 
 |-  { <. A , C >. , <. B , D >. } = ( { <. A , C >. } u. { <. B , D >. } )
15 14 funeqi 
 |-  ( Fun { <. A , C >. , <. B , D >. } <-> Fun ( { <. A , C >. } u. { <. B , D >. } ) )
16 13 15 sylibr 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> Fun { <. A , C >. , <. B , D >. } )