Description: The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014) (Revised by Mario Carneiro, 31-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fvssunirn | ⊢ ( 𝐹 ‘ 𝑋 ) ⊆ ∪ ran 𝐹 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvrn0 | ⊢ ( 𝐹 ‘ 𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } ) | |
| 2 | elssuni | ⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } ) → ( 𝐹 ‘ 𝑋 ) ⊆ ∪ ( ran 𝐹 ∪ { ∅ } ) ) | |
| 3 | 1 2 | ax-mp | ⊢ ( 𝐹 ‘ 𝑋 ) ⊆ ∪ ( ran 𝐹 ∪ { ∅ } ) |
| 4 | uniun | ⊢ ∪ ( ran 𝐹 ∪ { ∅ } ) = ( ∪ ran 𝐹 ∪ ∪ { ∅ } ) | |
| 5 | 0ex | ⊢ ∅ ∈ V | |
| 6 | 5 | unisn | ⊢ ∪ { ∅ } = ∅ |
| 7 | 6 | uneq2i | ⊢ ( ∪ ran 𝐹 ∪ ∪ { ∅ } ) = ( ∪ ran 𝐹 ∪ ∅ ) |
| 8 | un0 | ⊢ ( ∪ ran 𝐹 ∪ ∅ ) = ∪ ran 𝐹 | |
| 9 | 4 7 8 | 3eqtri | ⊢ ∪ ( ran 𝐹 ∪ { ∅ } ) = ∪ ran 𝐹 |
| 10 | 3 9 | sseqtri | ⊢ ( 𝐹 ‘ 𝑋 ) ⊆ ∪ ran 𝐹 |