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

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