Theorem fntp

Description: A function with a domain of three elements. (Contributed by NM, 14-Sep-2011) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	fntp.1	|- A e. _V
	fntp.2	|- B e. _V
	fntp.3	|- C e. _V
	fntp.4	|- D e. _V
	fntp.5	|- E e. _V
	fntp.6	|- F e. _V
Assertion	fntp	|- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { <. A , D >. , <. B , E >. , <. C , F >. } Fn { A , B , C } )

Proof

Step	Hyp	Ref	Expression
1		fntp.1	|- A e. _V
2		fntp.2	|- B e. _V
3		fntp.3	|- C e. _V
4		fntp.4	|- D e. _V
5		fntp.5	|- E e. _V
6		fntp.6	|- F e. _V
7	1 2 3 4 5 6	funtp	|- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> Fun { <. A , D >. , <. B , E >. , <. C , F >. } )
8	4 5 6	dmtpop	|- dom { <. A , D >. , <. B , E >. , <. C , F >. } = { A , B , C }
9		df-fn	|- ( { <. A , D >. , <. B , E >. , <. C , F >. } Fn { A , B , C } <-> ( Fun { <. A , D >. , <. B , E >. , <. C , F >. } /\ dom { <. A , D >. , <. B , E >. , <. C , F >. } = { A , B , C } ) )
10	7 8 9	sylanblrc	|- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { <. A , D >. , <. B , E >. , <. C , F >. } Fn { A , B , C } )