This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashimarni

Description: If 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 is a nonnegative integer, the size of the function F is the same nonnegative integer. (Contributed by Alexander van der Vekens, 4-Feb-2018)

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

Proof

Step Hyp Ref Expression
1 fveqeq2 
 |-  ( P = ( E " ran F ) -> ( ( # ` P ) = N <-> ( # ` ( E " ran F ) ) = N ) )
2 1 adantl 
 |-  ( ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E /\ ( E : dom E -1-1-> ran E /\ E e. V ) ) /\ P = ( E " ran F ) ) -> ( ( # ` P ) = N <-> ( # ` ( E " ran F ) ) = N ) )
3 hashimarn 
 |-  ( ( E : dom E -1-1-> ran E /\ E e. V ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E -> ( # ` ( E " ran F ) ) = ( # ` F ) ) )
4 3 impcom 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E /\ ( E : dom E -1-1-> ran E /\ E e. V ) ) -> ( # ` ( E " ran F ) ) = ( # ` F ) )
5 id 
 |-  ( ( # ` ( E " ran F ) ) = N -> ( # ` ( E " ran F ) ) = N )
6 4 5 sylan9req 
 |-  ( ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E /\ ( E : dom E -1-1-> ran E /\ E e. V ) ) /\ ( # ` ( E " ran F ) ) = N ) -> ( # ` F ) = N )
7 6 ex 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E /\ ( E : dom E -1-1-> ran E /\ E e. V ) ) -> ( ( # ` ( E " ran F ) ) = N -> ( # ` F ) = N ) )
8 7 adantr 
 |-  ( ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E /\ ( E : dom E -1-1-> ran E /\ E e. V ) ) /\ P = ( E " ran F ) ) -> ( ( # ` ( E " ran F ) ) = N -> ( # ` F ) = N ) )
9 2 8 sylbid 
 |-  ( ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E /\ ( E : dom E -1-1-> ran E /\ E e. V ) ) /\ P = ( E " ran F ) ) -> ( ( # ` P ) = N -> ( # ` F ) = N ) )
10 9 exp31 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E -> ( ( E : dom E -1-1-> ran E /\ E e. V ) -> ( P = ( E " ran F ) -> ( ( # ` P ) = N -> ( # ` F ) = N ) ) ) )
11 10 com23 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E -> ( P = ( E " ran F ) -> ( ( E : dom E -1-1-> ran E /\ E e. V ) -> ( ( # ` P ) = N -> ( # ` F ) = N ) ) ) )
12 11 com34 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E -> ( P = ( E " ran F ) -> ( ( # ` P ) = N -> ( ( E : dom E -1-1-> ran E /\ E e. V ) -> ( # ` F ) = N ) ) ) )
13 12 3imp 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E /\ P = ( E " ran F ) /\ ( # ` P ) = N ) -> ( ( E : dom E -1-1-> ran E /\ E e. V ) -> ( # ` F ) = N ) )
14 13 com12 
 |-  ( ( E : dom E -1-1-> ran E /\ E e. V ) -> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom E /\ P = ( E " ran F ) /\ ( # ` P ) = N ) -> ( # ` F ) = N ) )