Step | Hyp | Ref
| Expression |
1 | | dmres 5960 |
. . . . . . . . 9
⊢ dom
(𝐹 ↾ {𝑋}) = ({𝑋} ∩ dom 𝐹) |
2 | | incom 4162 |
. . . . . . . . 9
⊢ ({𝑋} ∩ dom 𝐹) = (dom 𝐹 ∩ {𝑋}) |
3 | 1, 2 | eqtri 2761 |
. . . . . . . 8
⊢ dom
(𝐹 ↾ {𝑋}) = (dom 𝐹 ∩ {𝑋}) |
4 | | disjsn 4673 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ dom 𝐹) |
5 | 4 | biimpri 227 |
. . . . . . . 8
⊢ (¬
𝑋 ∈ dom 𝐹 → (dom 𝐹 ∩ {𝑋}) = ∅) |
6 | 3, 5 | eqtrid 2785 |
. . . . . . 7
⊢ (¬
𝑋 ∈ dom 𝐹 → dom (𝐹 ↾ {𝑋}) = ∅) |
7 | 6 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → dom (𝐹 ↾ {𝑋}) = ∅) |
8 | | relres 5967 |
. . . . . . 7
⊢ Rel
(𝐹 ↾ {𝑋}) |
9 | | reldm0 5884 |
. . . . . . 7
⊢ (Rel
(𝐹 ↾ {𝑋}) → ((𝐹 ↾ {𝑋}) = ∅ ↔ dom (𝐹 ↾ {𝑋}) = ∅)) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢ ((𝐹 ↾ {𝑋}) = ∅ ↔ dom (𝐹 ↾ {𝑋}) = ∅) |
11 | 7, 10 | sylibr 233 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (𝐹 ↾ {𝑋}) = ∅) |
12 | | fnsng 6554 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {⟨𝑋, 𝑌⟩} Fn {𝑋}) |
13 | 12 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → {⟨𝑋, 𝑌⟩} Fn {𝑋}) |
14 | | fnresdm 6621 |
. . . . . 6
⊢
({⟨𝑋, 𝑌⟩} Fn {𝑋} → ({⟨𝑋, 𝑌⟩} ↾ {𝑋}) = {⟨𝑋, 𝑌⟩}) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ({⟨𝑋, 𝑌⟩} ↾ {𝑋}) = {⟨𝑋, 𝑌⟩}) |
16 | 11, 15 | uneq12d 4125 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ↾ {𝑋}) ∪ ({⟨𝑋, 𝑌⟩} ↾ {𝑋})) = (∅ ∪ {⟨𝑋, 𝑌⟩})) |
17 | | resundir 5953 |
. . . 4
⊢ ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋}) = ((𝐹 ↾ {𝑋}) ∪ ({⟨𝑋, 𝑌⟩} ↾ {𝑋})) |
18 | | uncom 4114 |
. . . . 5
⊢ (∅
∪ {⟨𝑋, 𝑌⟩}) = ({⟨𝑋, 𝑌⟩} ∪ ∅) |
19 | | un0 4351 |
. . . . 5
⊢
({⟨𝑋, 𝑌⟩} ∪ ∅) =
{⟨𝑋, 𝑌⟩} |
20 | 18, 19 | eqtr2i 2762 |
. . . 4
⊢
{⟨𝑋, 𝑌⟩} = (∅ ∪
{⟨𝑋, 𝑌⟩}) |
21 | 16, 17, 20 | 3eqtr4g 2798 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋}) = {⟨𝑋, 𝑌⟩}) |
22 | 21 | fveq1d 6845 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋})‘𝑋) = ({⟨𝑋, 𝑌⟩}‘𝑋)) |
23 | | snidg 4621 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
24 | 23 | 3ad2ant1 1134 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → 𝑋 ∈ {𝑋}) |
25 | 24 | fvresd 6863 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋})‘𝑋) = ((𝐹 ∪ {⟨𝑋, 𝑌⟩})‘𝑋)) |
26 | | fvsng 7127 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ({⟨𝑋, 𝑌⟩}‘𝑋) = 𝑌) |
27 | 26 | 3adant3 1133 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ({⟨𝑋, 𝑌⟩}‘𝑋) = 𝑌) |
28 | 22, 25, 27 | 3eqtr3d 2781 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌) |