Metamath Proof Explorer

Theorem funtpg

Description: A set of three pairs is a function if their first members are different. (Contributed by Alexander van der Vekens, 5-Dec-2017) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion funtpg 
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Fun { <. X , A >. , <. Y , B >. , <. Z , C >. } )

Proof

Step Hyp Ref Expression
1 3simpa 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( X e. U /\ Y e. V ) )
2 3simpa 
 |-  ( ( A e. F /\ B e. G /\ C e. H ) -> ( A e. F /\ B e. G ) )
3 simp1 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> X =/= Y )
4 funprg 
 |-  ( ( ( X e. U /\ Y e. V ) /\ ( A e. F /\ B e. G ) /\ X =/= Y ) -> Fun { <. X , A >. , <. Y , B >. } )
5 1 2 3 4 syl3an 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Fun { <. X , A >. , <. Y , B >. } )
6 simp3 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> Z e. W )
7 simp3 
 |-  ( ( A e. F /\ B e. G /\ C e. H ) -> C e. H )
8 funsng 
 |-  ( ( Z e. W /\ C e. H ) -> Fun { <. Z , C >. } )
9 6 7 8 syl2an 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) ) -> Fun { <. Z , C >. } )
10 9 3adant3 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Fun { <. Z , C >. } )
11 dmpropg 
 |-  ( ( A e. F /\ B e. G ) -> dom { <. X , A >. , <. Y , B >. } = { X , Y } )
12 dmsnopg 
 |-  ( C e. H -> dom { <. Z , C >. } = { Z } )
13 11 12 ineqan12d 
 |-  ( ( ( A e. F /\ B e. G ) /\ C e. H ) -> ( dom { <. X , A >. , <. Y , B >. } i^i dom { <. Z , C >. } ) = ( { X , Y } i^i { Z } ) )
14 13 3impa 
 |-  ( ( A e. F /\ B e. G /\ C e. H ) -> ( dom { <. X , A >. , <. Y , B >. } i^i dom { <. Z , C >. } ) = ( { X , Y } i^i { Z } ) )
15 disjprsn 
 |-  ( ( X =/= Z /\ Y =/= Z ) -> ( { X , Y } i^i { Z } ) = (/) )
16 15 3adant1 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( { X , Y } i^i { Z } ) = (/) )
17 14 16 sylan9eq 
 |-  ( ( ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( dom { <. X , A >. , <. Y , B >. } i^i dom { <. Z , C >. } ) = (/) )
18 17 3adant1 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( dom { <. X , A >. , <. Y , B >. } i^i dom { <. Z , C >. } ) = (/) )
19 funun 
 |-  ( ( ( Fun { <. X , A >. , <. Y , B >. } /\ Fun { <. Z , C >. } ) /\ ( dom { <. X , A >. , <. Y , B >. } i^i dom { <. Z , C >. } ) = (/) ) -> Fun ( { <. X , A >. , <. Y , B >. } u. { <. Z , C >. } ) )
20 5 10 18 19 syl21anc 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Fun ( { <. X , A >. , <. Y , B >. } u. { <. Z , C >. } ) )
21 df-tp 
 |-  { <. X , A >. , <. Y , B >. , <. Z , C >. } = ( { <. X , A >. , <. Y , B >. } u. { <. Z , C >. } )
22 21 funeqi 
 |-  ( Fun { <. X , A >. , <. Y , B >. , <. Z , C >. } <-> Fun ( { <. X , A >. , <. Y , B >. } u. { <. Z , C >. } ) )
23 20 22 sylibr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Fun { <. X , A >. , <. Y , B >. , <. Z , C >. } )