Proof of Theorem funiunfv
Step | Hyp | Ref
| Expression |
1 | | funres 6422 |
. . . 4
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝐴)) |
2 | 1 | funfnd 6411 |
. . 3
⊢ (Fun
𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
3 | | fniunfv 7060 |
. . 3
⊢ ((𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴) → ∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) = ∪ ran (𝐹 ↾ 𝐴)) |
4 | 2, 3 | syl 17 |
. 2
⊢ (Fun
𝐹 → ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) = ∪ ran (𝐹 ↾ 𝐴)) |
5 | | undif2 4391 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = (dom (𝐹 ↾ 𝐴) ∪ 𝐴) |
6 | | dmres 5873 |
. . . . . . 7
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
7 | | inss1 4143 |
. . . . . . 7
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
8 | 6, 7 | eqsstri 3935 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
9 | | ssequn1 4094 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 ↔ (dom (𝐹 ↾ 𝐴) ∪ 𝐴) = 𝐴) |
10 | 8, 9 | mpbi 233 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) ∪ 𝐴) = 𝐴 |
11 | 5, 10 | eqtri 2765 |
. . . 4
⊢ (dom
(𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = 𝐴 |
12 | | iuneq1 4920 |
. . . 4
⊢ ((dom
(𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = 𝐴 → ∪
𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥)) |
13 | 11, 12 | ax-mp 5 |
. . 3
⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥) |
14 | | iunxun 5002 |
. . . 4
⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = (∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪
𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) |
15 | | eldifn 4042 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴)) → ¬ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) |
16 | | ndmfv 6747 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ dom (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑥) = ∅) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴)) → ((𝐹 ↾ 𝐴)‘𝑥) = ∅) |
18 | 17 | iuneq2i 4925 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))∅ |
19 | | iun0 4970 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))∅ = ∅ |
20 | 18, 19 | eqtri 2765 |
. . . . . 6
⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥) = ∅ |
21 | 20 | uneq2i 4074 |
. . . . 5
⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪
𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) = (∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∅) |
22 | | un0 4305 |
. . . . 5
⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∅) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
23 | 21, 22 | eqtri 2765 |
. . . 4
⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪
𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) = ∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
24 | 14, 23 | eqtri 2765 |
. . 3
⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
25 | | fvres 6736 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
26 | 25 | iuneq2i 4925 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) |
27 | 13, 24, 26 | 3eqtr3ri 2774 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
28 | | df-ima 5564 |
. . 3
⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) |
29 | 28 | unieqi 4832 |
. 2
⊢ ∪ (𝐹
“ 𝐴) = ∪ ran (𝐹 ↾ 𝐴) |
30 | 4, 27, 29 | 3eqtr4g 2803 |
1
⊢ (Fun
𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴)) |