Metamath Proof Explorer

Theorem funcnvs4

Description: The converse of a length 4 word is a function if its symbols are different sets. (Contributed by AV, 10-Feb-2021)

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

Proof

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