Metamath Proof Explorer


Theorem funcnvs2

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

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

Proof

Step Hyp Ref Expression
1 c0ex
 |-  0 e. _V
2 1ex
 |-  1 e. _V
3 simp3
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> A =/= B )
4 funcnvpr
 |-  ( ( 0 e. _V /\ 1 e. _V /\ A =/= B ) -> Fun `' { <. 0 , A >. , <. 1 , B >. } )
5 1 2 3 4 mp3an12i
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> Fun `' { <. 0 , A >. , <. 1 , B >. } )
6 s2prop
 |-  ( ( A e. V /\ B e. V ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
7 6 3adant3
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
8 7 cnveqd
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> `' <" A B "> = `' { <. 0 , A >. , <. 1 , B >. } )
9 8 funeqd
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( Fun `' <" A B "> <-> Fun `' { <. 0 , A >. , <. 1 , B >. } ) )
10 5 9 mpbird
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> Fun `' <" A B "> )