Metamath Proof Explorer


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 "> )