Step | Hyp | Ref
| Expression |
1 | | dmres 4929 |
. . . . . . . . 9
⊢ dom
(𝐹 ↾ {𝑋}) = ({𝑋} ∩ dom 𝐹) |
2 | | incom 3328 |
. . . . . . . . 9
⊢ ({𝑋} ∩ dom 𝐹) = (dom 𝐹 ∩ {𝑋}) |
3 | 1, 2 | eqtri 2198 |
. . . . . . . 8
⊢ dom
(𝐹 ↾ {𝑋}) = (dom 𝐹 ∩ {𝑋}) |
4 | | disjsn 3655 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ dom 𝐹) |
5 | 4 | biimpri 133 |
. . . . . . . 8
⊢ (¬
𝑋 ∈ dom 𝐹 → (dom 𝐹 ∩ {𝑋}) = ∅) |
6 | 3, 5 | eqtrid 2222 |
. . . . . . 7
⊢ (¬
𝑋 ∈ dom 𝐹 → dom (𝐹 ↾ {𝑋}) = ∅) |
7 | 6 | 3ad2ant3 1020 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → dom (𝐹 ↾ {𝑋}) = ∅) |
8 | | relres 4936 |
. . . . . . 7
⊢ Rel
(𝐹 ↾ {𝑋}) |
9 | | reldm0 4846 |
. . . . . . 7
⊢ (Rel
(𝐹 ↾ {𝑋}) → ((𝐹 ↾ {𝑋}) = ∅ ↔ dom (𝐹 ↾ {𝑋}) = ∅)) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢ ((𝐹 ↾ {𝑋}) = ∅ ↔ dom (𝐹 ↾ {𝑋}) = ∅) |
11 | 7, 10 | sylibr 134 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (𝐹 ↾ {𝑋}) = ∅) |
12 | | fnsng 5264 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {⟨𝑋, 𝑌⟩} Fn {𝑋}) |
13 | 12 | 3adant3 1017 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → {⟨𝑋, 𝑌⟩} Fn {𝑋}) |
14 | | fnresdm 5326 |
. . . . . 6
⊢
({⟨𝑋, 𝑌⟩} Fn {𝑋} → ({⟨𝑋, 𝑌⟩} ↾ {𝑋}) = {⟨𝑋, 𝑌⟩}) |
15 | 13, 14 | syl 14 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ({⟨𝑋, 𝑌⟩} ↾ {𝑋}) = {⟨𝑋, 𝑌⟩}) |
16 | 11, 15 | uneq12d 3291 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ↾ {𝑋}) ∪ ({⟨𝑋, 𝑌⟩} ↾ {𝑋})) = (∅ ∪ {⟨𝑋, 𝑌⟩})) |
17 | | resundir 4922 |
. . . 4
⊢ ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋}) = ((𝐹 ↾ {𝑋}) ∪ ({⟨𝑋, 𝑌⟩} ↾ {𝑋})) |
18 | | uncom 3280 |
. . . . 5
⊢ (∅
∪ {⟨𝑋, 𝑌⟩}) = ({⟨𝑋, 𝑌⟩} ∪ ∅) |
19 | | un0 3457 |
. . . . 5
⊢
({⟨𝑋, 𝑌⟩} ∪ ∅) =
{⟨𝑋, 𝑌⟩} |
20 | 18, 19 | eqtr2i 2199 |
. . . 4
⊢
{⟨𝑋, 𝑌⟩} = (∅ ∪
{⟨𝑋, 𝑌⟩}) |
21 | 16, 17, 20 | 3eqtr4g 2235 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋}) = {⟨𝑋, 𝑌⟩}) |
22 | 21 | fveq1d 5518 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋})‘𝑋) = ({⟨𝑋, 𝑌⟩}‘𝑋)) |
23 | | snidg 3622 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
24 | 23 | 3ad2ant1 1018 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → 𝑋 ∈ {𝑋}) |
25 | | fvres 5540 |
. . 3
⊢ (𝑋 ∈ {𝑋} → (((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋})‘𝑋) = ((𝐹 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)) |
26 | 24, 25 | syl 14 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋})‘𝑋) = ((𝐹 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)) |
27 | | fvsng 5713 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ({⟨𝑋, 𝑌⟩}‘𝑋) = 𝑌) |
28 | 27 | 3adant3 1017 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ({⟨𝑋, 𝑌⟩}‘𝑋) = 𝑌) |
29 | 22, 26, 28 | 3eqtr3d 2218 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌) |