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 | ⊢ 𝐹 : 𝐶 ⟶ 𝒫 𝐵 | |
| Assertion | fpwfvss | ⊢ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐵 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fpwfvss.f | ⊢ 𝐹 : 𝐶 ⟶ 𝒫 𝐵 | |
| 2 | 1 | ffvelcdmi | ⊢ ( 𝐴 ∈ 𝐶 → ( 𝐹 ‘ 𝐴 ) ∈ 𝒫 𝐵 ) |
| 3 | 2 | elpwid | ⊢ ( 𝐴 ∈ 𝐶 → ( 𝐹 ‘ 𝐴 ) ⊆ 𝐵 ) |
| 4 | 1 | fdmi | ⊢ dom 𝐹 = 𝐶 |
| 5 | 4 | eleq2i | ⊢ ( 𝐴 ∈ dom 𝐹 ↔ 𝐴 ∈ 𝐶 ) |
| 6 | ndmfv | ⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ ) | |
| 7 | 5 6 | sylnbir | ⊢ ( ¬ 𝐴 ∈ 𝐶 → ( 𝐹 ‘ 𝐴 ) = ∅ ) |
| 8 | 0ss | ⊢ ∅ ⊆ 𝐵 | |
| 9 | 7 8 | eqsstrdi | ⊢ ( ¬ 𝐴 ∈ 𝐶 → ( 𝐹 ‘ 𝐴 ) ⊆ 𝐵 ) |
| 10 | 3 9 | pm2.61i | ⊢ ( 𝐹 ‘ 𝐴 ) ⊆ 𝐵 |