This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ftpg

Description: A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017)

Ref Expression
Assertion ftpg 
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { <. X , A >. , <. Y , B >. , <. Z , C >. } : { X , Y , Z } --> { A , B , 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 fprg 
 |-  ( ( ( X e. U /\ Y e. V ) /\ ( A e. F /\ B e. G ) /\ X =/= Y ) -> { <. X , A >. , <. Y , B >. } : { X , Y } --> { A , 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 ) ) -> { <. X , A >. , <. Y , B >. } : { X , Y } --> { A , B } )
6 eqidd 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { <. Z , C >. } = { <. Z , C >. } )
7 simp3 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> Z e. W )
8 simp3 
 |-  ( ( A e. F /\ B e. G /\ C e. H ) -> C e. H )
9 7 8 anim12i 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) ) -> ( Z e. W /\ C e. H ) )
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 ) ) -> ( Z e. W /\ C e. H ) )
11 fsng 
 |-  ( ( Z e. W /\ C e. H ) -> ( { <. Z , C >. } : { Z } --> { C } <-> { <. Z , C >. } = { <. Z , C >. } ) )
12 10 11 syl 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( { <. Z , C >. } : { Z } --> { C } <-> { <. Z , C >. } = { <. Z , C >. } ) )
13 6 12 mpbird 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { <. Z , C >. } : { Z } --> { C } )
14 elpri 
 |-  ( Z e. { X , Y } -> ( Z = X \/ Z = Y ) )
15 eqcom 
 |-  ( Z = X <-> X = Z )
16 nne 
 |-  ( -. X =/= Z <-> X = Z )
17 15 16 bitr4i 
 |-  ( Z = X <-> -. X =/= Z )
18 eqcom 
 |-  ( Z = Y <-> Y = Z )
19 nne 
 |-  ( -. Y =/= Z <-> Y = Z )
20 18 19 bitr4i 
 |-  ( Z = Y <-> -. Y =/= Z )
21 17 20 orbi12i 
 |-  ( ( Z = X \/ Z = Y ) <-> ( -. X =/= Z \/ -. Y =/= Z ) )
22 ianor 
 |-  ( -. ( X =/= Z /\ Y =/= Z ) <-> ( -. X =/= Z \/ -. Y =/= Z ) )
23 21 22 sylbb2 
 |-  ( ( Z = X \/ Z = Y ) -> -. ( X =/= Z /\ Y =/= Z ) )
24 14 23 syl 
 |-  ( Z e. { X , Y } -> -. ( X =/= Z /\ Y =/= Z ) )
25 24 con2i 
 |-  ( ( X =/= Z /\ Y =/= Z ) -> -. Z e. { X , Y } )
26 25 3adant1 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> -. Z e. { X , Y } )
27 26 3ad2ant3 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> -. Z e. { X , Y } )
28 disjsn 
 |-  ( ( { X , Y } i^i { Z } ) = (/) <-> -. Z e. { X , Y } )
29 27 28 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 ) ) -> ( { X , Y } i^i { Z } ) = (/) )
30 fun 
 |-  ( ( ( { <. X , A >. , <. Y , B >. } : { X , Y } --> { A , B } /\ { <. Z , C >. } : { Z } --> { C } ) /\ ( { X , Y } i^i { Z } ) = (/) ) -> ( { <. X , A >. , <. Y , B >. } u. { <. Z , C >. } ) : ( { X , Y } u. { Z } ) --> ( { A , B } u. { C } ) )
31 5 13 29 30 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 ) ) -> ( { <. X , A >. , <. Y , B >. } u. { <. Z , C >. } ) : ( { X , Y } u. { Z } ) --> ( { A , B } u. { C } ) )
32 df-tp 
 |-  { <. X , A >. , <. Y , B >. , <. Z , C >. } = ( { <. X , A >. , <. Y , B >. } u. { <. Z , C >. } )
33 32 feq1i 
 |-  ( { <. X , A >. , <. Y , B >. , <. Z , C >. } : { X , Y , Z } --> { A , B , C } <-> ( { <. X , A >. , <. Y , B >. } u. { <. Z , C >. } ) : { X , Y , Z } --> { A , B , C } )
34 df-tp 
 |-  { X , Y , Z } = ( { X , Y } u. { Z } )
35 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
36 34 35 feq23i 
 |-  ( ( { <. X , A >. , <. Y , B >. } u. { <. Z , C >. } ) : { X , Y , Z } --> { A , B , C } <-> ( { <. X , A >. , <. Y , B >. } u. { <. Z , C >. } ) : ( { X , Y } u. { Z } ) --> ( { A , B } u. { C } ) )
37 33 36 bitri 
 |-  ( { <. X , A >. , <. Y , B >. , <. Z , C >. } : { X , Y , Z } --> { A , B , C } <-> ( { <. X , A >. , <. Y , B >. } u. { <. Z , C >. } ) : ( { X , Y } u. { Z } ) --> ( { A , B } u. { C } ) )
38 31 37 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 ) ) -> { <. X , A >. , <. Y , B >. , <. Z , C >. } : { X , Y , Z } --> { A , B , C } )