Metamath Proof Explorer

Theorem mvhf1

Description: The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mvhf.v 
|- V = ( mVR ` T )
mvhf.e 
|- E = ( mEx ` T )
mvhf.h 
|- H = ( mVH ` T )
Assertion mvhf1 
|- ( T e. mFS -> H : V -1-1-> E )

Proof

Step Hyp Ref Expression
1 mvhf.v 
 |-  V = ( mVR ` T )
2 mvhf.e 
 |-  E = ( mEx ` T )
3 mvhf.h 
 |-  H = ( mVH ` T )
4 1 2 3 mvhf 
 |-  ( T e. mFS -> H : V --> E )
5 eqid 
 |-  ( mType ` T ) = ( mType ` T )
6 1 5 3 mvhval 
 |-  ( v e. V -> ( H ` v ) = <. ( ( mType ` T ) ` v ) , <" v "> >. )
7 1 5 3 mvhval 
 |-  ( w e. V -> ( H ` w ) = <. ( ( mType ` T ) ` w ) , <" w "> >. )
8 6 7 eqeqan12d 
 |-  ( ( v e. V /\ w e. V ) -> ( ( H ` v ) = ( H ` w ) <-> <. ( ( mType ` T ) ` v ) , <" v "> >. = <. ( ( mType ` T ) ` w ) , <" w "> >. ) )
9 8 adantl 
 |-  ( ( T e. mFS /\ ( v e. V /\ w e. V ) ) -> ( ( H ` v ) = ( H ` w ) <-> <. ( ( mType ` T ) ` v ) , <" v "> >. = <. ( ( mType ` T ) ` w ) , <" w "> >. ) )
10 fvex 
 |-  ( ( mType ` T ) ` v ) e. _V
11 s1cli 
 |-  <" v "> e. Word _V
12 11 elexi 
 |-  <" v "> e. _V
13 10 12 opth 
 |-  ( <. ( ( mType ` T ) ` v ) , <" v "> >. = <. ( ( mType ` T ) ` w ) , <" w "> >. <-> ( ( ( mType ` T ) ` v ) = ( ( mType ` T ) ` w ) /\ <" v "> = <" w "> ) )
14 13 simprbi 
 |-  ( <. ( ( mType ` T ) ` v ) , <" v "> >. = <. ( ( mType ` T ) ` w ) , <" w "> >. -> <" v "> = <" w "> )
15 s111 
 |-  ( ( v e. V /\ w e. V ) -> ( <" v "> = <" w "> <-> v = w ) )
16 15 adantl 
 |-  ( ( T e. mFS /\ ( v e. V /\ w e. V ) ) -> ( <" v "> = <" w "> <-> v = w ) )
17 14 16 imbitrid 
 |-  ( ( T e. mFS /\ ( v e. V /\ w e. V ) ) -> ( <. ( ( mType ` T ) ` v ) , <" v "> >. = <. ( ( mType ` T ) ` w ) , <" w "> >. -> v = w ) )
18 9 17 sylbid 
 |-  ( ( T e. mFS /\ ( v e. V /\ w e. V ) ) -> ( ( H ` v ) = ( H ` w ) -> v = w ) )
19 18 ralrimivva 
 |-  ( T e. mFS -> A. v e. V A. w e. V ( ( H ` v ) = ( H ` w ) -> v = w ) )
20 dff13 
 |-  ( H : V -1-1-> E <-> ( H : V --> E /\ A. v e. V A. w e. V ( ( H ` v ) = ( H ` w ) -> v = w ) ) )
21 4 19 20 sylanbrc 
 |-  ( T e. mFS -> H : V -1-1-> E )