Description: The indexed union of a function's values is the union of its image under the index class.
Note: This theorem depends on the fact that our function value is the empty set outside of its domain. If the antecedent is changed to F Fn A , the theorem can be proved without this dependency. (Contributed by NM, 26-Mar-2006) (Proof shortened by Mario Carneiro, 31-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | funiunfv | ⊢ ( Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∪ ( 𝐹 “ 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funres | ⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐴 ) ) | |
| 2 | 1 | funfnd | ⊢ ( Fun 𝐹 → ( 𝐹 ↾ 𝐴 ) Fn dom ( 𝐹 ↾ 𝐴 ) ) |
| 3 | fniunfv | ⊢ ( ( 𝐹 ↾ 𝐴 ) Fn dom ( 𝐹 ↾ 𝐴 ) → ∪ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ∪ ran ( 𝐹 ↾ 𝐴 ) ) | |
| 4 | 2 3 | syl | ⊢ ( Fun 𝐹 → ∪ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ∪ ran ( 𝐹 ↾ 𝐴 ) ) |
| 5 | undif2 | ⊢ ( dom ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ) = ( dom ( 𝐹 ↾ 𝐴 ) ∪ 𝐴 ) | |
| 6 | dmres | ⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 ) | |
| 7 | inss1 | ⊢ ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴 | |
| 8 | 6 7 | eqsstri | ⊢ dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 |
| 9 | ssequn1 | ⊢ ( dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 ↔ ( dom ( 𝐹 ↾ 𝐴 ) ∪ 𝐴 ) = 𝐴 ) | |
| 10 | 8 9 | mpbi | ⊢ ( dom ( 𝐹 ↾ 𝐴 ) ∪ 𝐴 ) = 𝐴 |
| 11 | 5 10 | eqtri | ⊢ ( dom ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ) = 𝐴 |
| 12 | iuneq1 | ⊢ ( ( dom ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ) = 𝐴 → ∪ 𝑥 ∈ ( dom ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ∪ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ) | |
| 13 | 11 12 | ax-mp | ⊢ ∪ 𝑥 ∈ ( dom ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ∪ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) |
| 14 | iunxun | ⊢ ∪ 𝑥 ∈ ( dom ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ∪ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∪ ∪ 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ) | |
| 15 | eldifn | ⊢ ( 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) → ¬ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) | |
| 16 | ndmfv | ⊢ ( ¬ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ∅ ) | |
| 17 | 15 16 | syl | ⊢ ( 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ∅ ) |
| 18 | 17 | iuneq2i | ⊢ ∪ 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ∪ 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ∅ |
| 19 | iun0 | ⊢ ∪ 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ∅ = ∅ | |
| 20 | 18 19 | eqtri | ⊢ ∪ 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ∅ |
| 21 | 20 | uneq2i | ⊢ ( ∪ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∪ ∪ 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ) = ( ∪ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∪ ∅ ) |
| 22 | un0 | ⊢ ( ∪ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∪ ∅ ) = ∪ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) | |
| 23 | 21 22 | eqtri | ⊢ ( ∪ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∪ ∪ 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ) = ∪ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) |
| 24 | 14 23 | eqtri | ⊢ ∪ 𝑥 ∈ ( dom ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹 ↾ 𝐴 ) ) ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ∪ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) |
| 25 | fvres | ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) | |
| 26 | 25 | iuneq2i | ⊢ ∪ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) |
| 27 | 13 24 26 | 3eqtr3ri | ⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∪ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) |
| 28 | df-ima | ⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 ) | |
| 29 | 28 | unieqi | ⊢ ∪ ( 𝐹 “ 𝐴 ) = ∪ ran ( 𝐹 ↾ 𝐴 ) |
| 30 | 4 27 29 | 3eqtr4g | ⊢ ( Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∪ ( 𝐹 “ 𝐴 ) ) |