Proof of Theorem funiunfv
Step | Hyp | Ref
| Expression |
1 | | funres 5929 |
. . . 4
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝐴)) |
2 | | funfn 5918 |
. . . 4
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
3 | 1, 2 | sylib 208 |
. . 3
⊢ (Fun
𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
4 | | fniunfv 6505 |
. . 3
⊢ ((𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴) → ∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) = ∪ ran (𝐹 ↾ 𝐴)) |
5 | 3, 4 | syl 17 |
. 2
⊢ (Fun
𝐹 → ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) = ∪ ran (𝐹 ↾ 𝐴)) |
6 | | undif2 4044 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = (dom (𝐹 ↾ 𝐴) ∪ 𝐴) |
7 | | dmres 5419 |
. . . . . . 7
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
8 | | inss1 3833 |
. . . . . . 7
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
9 | 7, 8 | eqsstri 3635 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
10 | | ssequn1 3783 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 ↔ (dom (𝐹 ↾ 𝐴) ∪ 𝐴) = 𝐴) |
11 | 9, 10 | mpbi 220 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) ∪ 𝐴) = 𝐴 |
12 | 6, 11 | eqtri 2644 |
. . . 4
⊢ (dom
(𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = 𝐴 |
13 | | iuneq1 4534 |
. . . 4
⊢ ((dom
(𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴))) = 𝐴 → ∪
𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥)) |
14 | 12, 13 | ax-mp 5 |
. . 3
⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥) |
15 | | iunxun 4605 |
. . . 4
⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = (∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪
𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) |
16 | | eldifn 3733 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴)) → ¬ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) |
17 | | ndmfv 6218 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ dom (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑥) = ∅) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴)) → ((𝐹 ↾ 𝐴)‘𝑥) = ∅) |
19 | 18 | iuneq2i 4539 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))∅ |
20 | | iun0 4576 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))∅ = ∅ |
21 | 19, 20 | eqtri 2644 |
. . . . . 6
⊢ ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥) = ∅ |
22 | 21 | uneq2i 3764 |
. . . . 5
⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪
𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) = (∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∅) |
23 | | un0 3967 |
. . . . 5
⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∅) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
24 | 22, 23 | eqtri 2644 |
. . . 4
⊢ (∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) ∪ ∪
𝑥 ∈ (𝐴 ∖ dom (𝐹 ↾ 𝐴))((𝐹 ↾ 𝐴)‘𝑥)) = ∪
𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
25 | 15, 24 | eqtri 2644 |
. . 3
⊢ ∪ 𝑥 ∈ (dom (𝐹 ↾ 𝐴) ∪ (𝐴 ∖ dom (𝐹 ↾ 𝐴)))((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
26 | | fvres 6207 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
27 | 26 | iuneq2i 4539 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐴)‘𝑥) = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) |
28 | 14, 25, 27 | 3eqtr3ri 2653 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ 𝑥 ∈ dom (𝐹 ↾ 𝐴)((𝐹 ↾ 𝐴)‘𝑥) |
29 | | df-ima 5127 |
. . 3
⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) |
30 | 29 | unieqi 4445 |
. 2
⊢ ∪ (𝐹
“ 𝐴) = ∪ ran (𝐹 ↾ 𝐴) |
31 | 5, 28, 30 | 3eqtr4g 2681 |
1
⊢ (Fun
𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴)) |