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

Metamath Proof Explorer

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