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

Metamath Proof Explorer

Theorem f1imaen3g

Description: If a set function is one-to-one, then a subset of its domain is equinumerous to the image of that subset. (This version of f1imaeng does not need ax-rep nor ax-pow .) (Contributed by BTernaryTau, 13-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 resexg 
 |-  ( F e. V -> ( F |` C ) e. _V )
2 1 3ad2ant3 
 |-  ( ( F : A -1-1-> B /\ C C_ A /\ F e. V ) -> ( F |` C ) e. _V )
3 f1ores 
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )
4 3 3adant3 
 |-  ( ( F : A -1-1-> B /\ C C_ A /\ F e. V ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )
5 f1oen3g 
 |-  ( ( ( F |` C ) e. _V /\ ( F |` C ) : C -1-1-onto-> ( F " C ) ) -> C ~~ ( F " C ) )
6 2 4 5 syl2anc 
 |-  ( ( F : A -1-1-> B /\ C C_ A /\ F e. V ) -> C ~~ ( F " C ) )