Theorem hashimaf1

Description: Taking the image of a set by a one-to-one function does not affect size. (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	hashimaf1.1	|- ( ph -> F : A -1-1-> B )
	hashimaf1.2	|- ( ph -> C C_ A )
	hashimaf1.3	|- ( ph -> A e. V )
Assertion	hashimaf1	|- ( ph -> ( # ` ( F " C ) ) = ( # ` C ) )

Proof

Step	Hyp	Ref	Expression
1		hashimaf1.1	|- ( ph -> F : A -1-1-> B )
2		hashimaf1.2	|- ( ph -> C C_ A )
3		hashimaf1.3	|- ( ph -> A e. V )
4	3 2	sselpwd	|- ( ph -> C e. ~P A )
5		f1ores	|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )
6	1 2 5	syl2anc	|- ( ph -> ( F |` C ) : C -1-1-onto-> ( F " C ) )
7		f1oeng	|- ( ( C e. ~P A /\ ( F |` C ) : C -1-1-onto-> ( F " C ) ) -> C ~~ ( F " C ) )
8	4 6 7	syl2anc	|- ( ph -> C ~~ ( F " C ) )
9	8	ensymd	|- ( ph -> ( F " C ) ~~ C )
10		hasheni	|- ( ( F " C ) ~~ C -> ( # ` ( F " C ) ) = ( # ` C ) )
11	9 10	syl	|- ( ph -> ( # ` ( F " C ) ) = ( # ` C ) )