Metamath Proof Explorer

Theorem hashimarn

Description: The size of the image of a one-to-one function E under the range of a function F which is a one-to-one function into the domain of E equals the size of the function F . (Contributed by Alexander van der Vekens, 4-Feb-2018) (Proof shortened by AV, 4-May-2021)

Ref Expression
Assertion hashimarn 
|- ( ( E : dom E -1-1-> ran E /\ E e. V ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E -> ( # ` ( E " ran F ) ) = ( # ` F ) ) )

Proof

Step Hyp Ref Expression
1 f1f 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E -> F : ( 0 ..^ ( # ` F ) ) --> dom E )
2 1 frnd 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E -> ran F C_ dom E )
3 2 adantl 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> ran F C_ dom E )
4 ssdmres 
 |-  ( ran F C_ dom E <-> dom ( E |` ran F ) = ran F )
5 3 4 sylib 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> dom ( E |` ran F ) = ran F )
6 5 fveq2d 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> ( # ` dom ( E |` ran F ) ) = ( # ` ran F ) )
7 df-ima 
 |-  ( E " ran F ) = ran ( E |` ran F )
8 7 fveq2i 
 |-  ( # ` ( E " ran F ) ) = ( # ` ran ( E |` ran F ) )
9 f1fun 
 |-  ( E : dom E -1-1-> ran E -> Fun E )
10 funres 
 |-  ( Fun E -> Fun ( E |` ran F ) )
11 10 funfnd 
 |-  ( Fun E -> ( E |` ran F ) Fn dom ( E |` ran F ) )
12 9 11 syl 
 |-  ( E : dom E -1-1-> ran E -> ( E |` ran F ) Fn dom ( E |` ran F ) )
13 12 ad2antrr 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> ( E |` ran F ) Fn dom ( E |` ran F ) )
14 hashfn 
 |-  ( ( E |` ran F ) Fn dom ( E |` ran F ) -> ( # ` ( E |` ran F ) ) = ( # ` dom ( E |` ran F ) ) )
15 13 14 syl 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> ( # ` ( E |` ran F ) ) = ( # ` dom ( E |` ran F ) ) )
16 ovex 
 |-  ( 0 ..^ ( # ` F ) ) e. _V
17 fex 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) --> dom E /\ ( 0 ..^ ( # ` F ) ) e. _V ) -> F e. _V )
18 1 16 17 sylancl 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E -> F e. _V )
19 rnexg 
 |-  ( F e. _V -> ran F e. _V )
20 18 19 syl 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E -> ran F e. _V )
21 simpll 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> E : dom E -1-1-> ran E )
22 f1ssres 
 |-  ( ( E : dom E -1-1-> ran E /\ ran F C_ dom E ) -> ( E |` ran F ) : ran F -1-1-> ran E )
23 21 3 22 syl2anc 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> ( E |` ran F ) : ran F -1-1-> ran E )
24 hashf1rn 
 |-  ( ( ran F e. _V /\ ( E |` ran F ) : ran F -1-1-> ran E ) -> ( # ` ( E |` ran F ) ) = ( # ` ran ( E |` ran F ) ) )
25 20 23 24 syl2an2 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> ( # ` ( E |` ran F ) ) = ( # ` ran ( E |` ran F ) ) )
26 15 25 eqtr3d 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> ( # ` dom ( E |` ran F ) ) = ( # ` ran ( E |` ran F ) ) )
27 8 26 eqtr4id 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> ( # ` ( E " ran F ) ) = ( # ` dom ( E |` ran F ) ) )
28 hashf1rn 
 |-  ( ( ( 0 ..^ ( # ` F ) ) e. _V /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> ( # ` F ) = ( # ` ran F ) )
29 16 28 mpan 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E -> ( # ` F ) = ( # ` ran F ) )
30 29 adantl 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> ( # ` F ) = ( # ` ran F ) )
31 6 27 30 3eqtr4d 
 |-  ( ( ( E : dom E -1-1-> ran E /\ E e. V ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E ) -> ( # ` ( E " ran F ) ) = ( # ` F ) )
32 31 ex 
 |-  ( ( E : dom E -1-1-> ran E /\ E e. V ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E -> ( # ` ( E " ran F ) ) = ( # ` F ) ) )