Metamath Proof Explorer

Theorem f1imaenfi

Description: If a function is one-to-one, then the image of a finite subset of its domain under it is equinumerous to the subset. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1imaeng ). (Contributed by BTernaryTau, 29-Sep-2024)

Ref Expression
Assertion f1imaenfi 
|- ( ( F : A -1-1-> B /\ C C_ A /\ C e. Fin ) -> ( F " C ) ~~ C )

Proof

Step Hyp Ref Expression
1 f1ores 
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )
2 f1oenfi 
 |-  ( ( C e. Fin /\ ( F |` C ) : C -1-1-onto-> ( F " C ) ) -> C ~~ ( F " C ) )
3 ensymfib 
 |-  ( C e. Fin -> ( C ~~ ( F " C ) <-> ( F " C ) ~~ C ) )
4 3 adantr 
 |-  ( ( C e. Fin /\ ( F |` C ) : C -1-1-onto-> ( F " C ) ) -> ( C ~~ ( F " C ) <-> ( F " C ) ~~ C ) )
5 2 4 mpbid 
 |-  ( ( C e. Fin /\ ( F |` C ) : C -1-1-onto-> ( F " C ) ) -> ( F " C ) ~~ C )
6 1 5 sylan2 
 |-  ( ( C e. Fin /\ ( F : A -1-1-> B /\ C C_ A ) ) -> ( F " C ) ~~ C )
7 6 3impb 
 |-  ( ( C e. Fin /\ F : A -1-1-> B /\ C C_ A ) -> ( F " C ) ~~ C )
8 7 3coml 
 |-  ( ( F : A -1-1-> B /\ C C_ A /\ C e. Fin ) -> ( F " C ) ~~ C )