Proof of Theorem funiunfv
Step | Hyp | Ref
| Expression |
1 | | funres 5843 |
. . . 4
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝐴)) |
2 | | funfn 5833 |
. . . 4
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
3 | 1, 2 | sylib 207 |
. . 3
⊢ (Fun
𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
4 | | fniunfv 6409 |
. . 3
⊢ ((𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴) → ∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) = ∪ ran (𝐹 ↾ 𝐴)) |
5 | 3, 4 | syl 17 |
. 2
⊢ (Fun
𝐹 → ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) = ∪ ran (𝐹 ↾ 𝐴)) |
6 | | undif2 3996 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = (dom (𝐹 ↾ 𝐴) ∪ 𝐴) |
7 | | dmres 5339 |
. . . . . . 7
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
8 | | inss1 3795 |
. . . . . . 7
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
9 | 7, 8 | eqsstri 3598 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
10 | | ssequn1 3745 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 ↔ (dom (𝐹 ↾ 𝐴) ∪ 𝐴) = 𝐴) |
11 | 9, 10 | mpbi 219 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) ∪ 𝐴) = 𝐴 |
12 | 6, 11 | eqtri 2632 |
. . . 4
⊢ (dom
(𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = 𝐴 |
13 | | iuneq1 4470 |
. . . 4
⊢ ((dom
(𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = 𝐴 → ∪
𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥)) |
14 | 12, 13 | ax-mp 5 |
. . 3
⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥) |
15 | | iunxun 4541 |
. . . 4
⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = (∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪
𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) |
16 | | eldifn 3695 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴)) → ¬ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) |
17 | | ndmfv 6128 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ dom (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑥) = ∅) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴)) → ((𝐹 ↾ 𝐴)‘𝑥) = ∅) |
19 | 18 | iuneq2i 4475 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))∅ |
20 | | iun0 4512 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))∅ = ∅ |
21 | 19, 20 | eqtri 2632 |
. . . . . 6
⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥) = ∅ |
22 | 21 | uneq2i 3726 |
. . . . 5
⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪
𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) = (∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∅) |
23 | | un0 3919 |
. . . . 5
⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∅) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
24 | 22, 23 | eqtri 2632 |
. . . 4
⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪
𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) = ∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
25 | 15, 24 | eqtri 2632 |
. . 3
⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
26 | | fvres 6117 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
27 | 26 | iuneq2i 4475 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) |
28 | 14, 25, 27 | 3eqtr3ri 2641 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
29 | | df-ima 5051 |
. . 3
⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) |
30 | 29 | unieqi 4381 |
. 2
⊢ ∪ (𝐹
“ 𝐴) = ∪ ran (𝐹 ↾ 𝐴) |
31 | 5, 28, 30 | 3eqtr4g 2669 |
1
⊢ (Fun
𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴)) |