Description: Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | foelrn | |- ( ( F : A -onto-> B /\ C e. B ) -> E. x e. A C = ( F ` x ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dffo3 | |- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) ) |
|
2 | 1 | simprbi | |- ( F : A -onto-> B -> A. y e. B E. x e. A y = ( F ` x ) ) |
3 | eqeq1 | |- ( y = C -> ( y = ( F ` x ) <-> C = ( F ` x ) ) ) |
|
4 | 3 | rexbidv | |- ( y = C -> ( E. x e. A y = ( F ` x ) <-> E. x e. A C = ( F ` x ) ) ) |
5 | 4 | rspccva | |- ( ( A. y e. B E. x e. A y = ( F ` x ) /\ C e. B ) -> E. x e. A C = ( F ` x ) ) |
6 | 2 5 | sylan | |- ( ( F : A -onto-> B /\ C e. B ) -> E. x e. A C = ( F ` x ) ) |