Theorem ftp

Description: A function with a domain of three elements. (Contributed by Stefan O'Rear, 17-Oct-2014) (Proof shortened by Alexander van der Vekens, 23-Jan-2018)

	Ref	Expression
Hypotheses	ftp.a	|- A e. _V
	ftp.b	|- B e. _V
	ftp.c	|- C e. _V
	ftp.d	|- X e. _V
	ftp.e	|- Y e. _V
	ftp.f	|- Z e. _V
	ftp.g	|- A =/= B
	ftp.h	|- A =/= C
	ftp.i	|- B =/= C
Assertion	ftp	|- { <. A , X >. , <. B , Y >. , <. C , Z >. } : { A , B , C } --> { X , Y , Z }

Proof

Step	Hyp	Ref	Expression
1		ftp.a	|- A e. _V
2		ftp.b	|- B e. _V
3		ftp.c	|- C e. _V
4		ftp.d	|- X e. _V
5		ftp.e	|- Y e. _V
6		ftp.f	|- Z e. _V
7		ftp.g	|- A =/= B
8		ftp.h	|- A =/= C
9		ftp.i	|- B =/= C
10	1 2 3	3pm3.2i	|- ( A e. _V /\ B e. _V /\ C e. _V )
11	4 5 6	3pm3.2i	|- ( X e. _V /\ Y e. _V /\ Z e. _V )
12	7 8 9	3pm3.2i	|- ( A =/= B /\ A =/= C /\ B =/= C )
13		ftpg	|- ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ ( X e. _V /\ Y e. _V /\ Z e. _V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> { <. A , X >. , <. B , Y >. , <. C , Z >. } : { A , B , C } --> { X , Y , Z } )
14	10 11 12 13	mp3an	|- { <. A , X >. , <. B , Y >. , <. C , Z >. } : { A , B , C } --> { X , Y , Z }