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