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