Description: Functions into a powerset always have values which are subsets. This is dependant on our convention when the argument is not part of the domain. (Contributed by RP, 13-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | fpwfvss.f | |- F : C --> ~P B |
|
| Assertion | fpwfvss | |- ( F ` A ) C_ B |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fpwfvss.f | |- F : C --> ~P B |
|
| 2 | 1 | ffvelcdmi | |- ( A e. C -> ( F ` A ) e. ~P B ) |
| 3 | 2 | elpwid | |- ( A e. C -> ( F ` A ) C_ B ) |
| 4 | 1 | fdmi | |- dom F = C |
| 5 | 4 | eleq2i | |- ( A e. dom F <-> A e. C ) |
| 6 | ndmfv | |- ( -. A e. dom F -> ( F ` A ) = (/) ) |
|
| 7 | 5 6 | sylnbir | |- ( -. A e. C -> ( F ` A ) = (/) ) |
| 8 | 0ss | |- (/) C_ B |
|
| 9 | 7 8 | eqsstrdi | |- ( -. A e. C -> ( F ` A ) C_ B ) |
| 10 | 3 9 | pm2.61i | |- ( F ` A ) C_ B |