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