Theorem funcnvs3

Description: The converse of a length 3 word is a function if its symbols are different sets. (Contributed by Alexander van der Vekens, 31-Jan-2018) (Revised by AV, 23-Jan-2021)

	Ref	Expression
Assertion	funcnvs3	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> Fun `' <" A B C "> )

Proof

Step	Hyp	Ref	Expression
1		c0ex	|- 0 e. _V
2		1ex	|- 1 e. _V
3		2ex	|- 2 e. _V
4	1 2 3	3pm3.2i	|- ( 0 e. _V /\ 1 e. _V /\ 2 e. _V )
5	4	a1i	|- ( ( A e. V /\ B e. V /\ C e. V ) -> ( 0 e. _V /\ 1 e. _V /\ 2 e. _V ) )
6		funcnvtp	|- ( ( ( 0 e. _V /\ 1 e. _V /\ 2 e. _V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> Fun `' { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } )
7	5 6	sylan	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> Fun `' { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } )
8		s3tpop	|- ( ( A e. V /\ B e. V /\ C e. V ) -> <" A B C "> = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } )
9	8	adantr	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> <" A B C "> = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } )
10	9	cnveqd	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> `' <" A B C "> = `' { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } )
11	10	funeqd	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( Fun `' <" A B C "> <-> Fun `' { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } ) )
12	7 11	mpbird	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> Fun `' <" A B C "> )