Metamath Proof Explorer

Theorem f1imaen2g

Description: A one-to-one function's image under a subset of its domain is equinumerous to the subset. (This version of f1imaen does not need ax-reg .) (Contributed by Mario Carneiro, 16-Nov-2014) (Revised by Mario Carneiro, 25-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 simprr 
 |-  ( ( ( F : A -1-1-> B /\ B e. V ) /\ ( C C_ A /\ C e. V ) ) -> C e. V )
2 simplr 
 |-  ( ( ( F : A -1-1-> B /\ B e. V ) /\ ( C C_ A /\ C e. V ) ) -> B e. V )
3 f1f 
 |-  ( F : A -1-1-> B -> F : A --> B )
4 fimass 
 |-  ( F : A --> B -> ( F " C ) C_ B )
5 3 4 syl 
 |-  ( F : A -1-1-> B -> ( F " C ) C_ B )
6 5 ad2antrr 
 |-  ( ( ( F : A -1-1-> B /\ B e. V ) /\ ( C C_ A /\ C e. V ) ) -> ( F " C ) C_ B )
7 2 6 ssexd 
 |-  ( ( ( F : A -1-1-> B /\ B e. V ) /\ ( C C_ A /\ C e. V ) ) -> ( F " C ) e. _V )
8 f1ores 
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )
9 8 ad2ant2r 
 |-  ( ( ( F : A -1-1-> B /\ B e. V ) /\ ( C C_ A /\ C e. V ) ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )
10 f1oen2g 
 |-  ( ( C e. V /\ ( F " C ) e. _V /\ ( F |` C ) : C -1-1-onto-> ( F " C ) ) -> C ~~ ( F " C ) )
11 1 7 9 10 syl3anc 
 |-  ( ( ( F : A -1-1-> B /\ B e. V ) /\ ( C C_ A /\ C e. V ) ) -> C ~~ ( F " C ) )
12 11 ensymd 
 |-  ( ( ( F : A -1-1-> B /\ B e. V ) /\ ( C C_ A /\ C e. V ) ) -> ( F " C ) ~~ C )