Description: A set is weakly dominant over its image under any function. (Contributed by Stefan O'Rear, 14-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | wdomimag | |- ( ( Fun F /\ A e. V ) -> ( F " A ) ~<_* A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funimaexg | |- ( ( Fun F /\ A e. V ) -> ( F " A ) e. _V ) |
|
2 | wdomima2g | |- ( ( Fun F /\ A e. V /\ ( F " A ) e. _V ) -> ( F " A ) ~<_* A ) |
|
3 | 1 2 | mpd3an3 | |- ( ( Fun F /\ A e. V ) -> ( F " A ) ~<_* A ) |