Proof of Theorem fsnunfv
| Step | Hyp | Ref
| Expression |
| 1 | | dmres 6030 |
. . . . . . . . 9
⊢ dom
(𝐹 ↾ {𝑋}) = ({𝑋} ∩ dom 𝐹) |
| 2 | | incom 4209 |
. . . . . . . . 9
⊢ ({𝑋} ∩ dom 𝐹) = (dom 𝐹 ∩ {𝑋}) |
| 3 | 1, 2 | eqtri 2765 |
. . . . . . . 8
⊢ dom
(𝐹 ↾ {𝑋}) = (dom 𝐹 ∩ {𝑋}) |
| 4 | | disjsn 4711 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ dom 𝐹) |
| 5 | 4 | biimpri 228 |
. . . . . . . 8
⊢ (¬
𝑋 ∈ dom 𝐹 → (dom 𝐹 ∩ {𝑋}) = ∅) |
| 6 | 3, 5 | eqtrid 2789 |
. . . . . . 7
⊢ (¬
𝑋 ∈ dom 𝐹 → dom (𝐹 ↾ {𝑋}) = ∅) |
| 7 | 6 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → dom (𝐹 ↾ {𝑋}) = ∅) |
| 8 | | relres 6023 |
. . . . . . 7
⊢ Rel
(𝐹 ↾ {𝑋}) |
| 9 | | reldm0 5938 |
. . . . . . 7
⊢ (Rel
(𝐹 ↾ {𝑋}) → ((𝐹 ↾ {𝑋}) = ∅ ↔ dom (𝐹 ↾ {𝑋}) = ∅)) |
| 10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢ ((𝐹 ↾ {𝑋}) = ∅ ↔ dom (𝐹 ↾ {𝑋}) = ∅) |
| 11 | 7, 10 | sylibr 234 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (𝐹 ↾ {𝑋}) = ∅) |
| 12 | | fnsng 6618 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {〈𝑋, 𝑌〉} Fn {𝑋}) |
| 13 | 12 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → {〈𝑋, 𝑌〉} Fn {𝑋}) |
| 14 | | fnresdm 6687 |
. . . . . 6
⊢
({〈𝑋, 𝑌〉} Fn {𝑋} → ({〈𝑋, 𝑌〉} ↾ {𝑋}) = {〈𝑋, 𝑌〉}) |
| 15 | 13, 14 | syl 17 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ({〈𝑋, 𝑌〉} ↾ {𝑋}) = {〈𝑋, 𝑌〉}) |
| 16 | 11, 15 | uneq12d 4169 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ↾ {𝑋}) ∪ ({〈𝑋, 𝑌〉} ↾ {𝑋})) = (∅ ∪ {〈𝑋, 𝑌〉})) |
| 17 | | resundir 6012 |
. . . 4
⊢ ((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ {𝑋}) = ((𝐹 ↾ {𝑋}) ∪ ({〈𝑋, 𝑌〉} ↾ {𝑋})) |
| 18 | | uncom 4158 |
. . . . 5
⊢ (∅
∪ {〈𝑋, 𝑌〉}) = ({〈𝑋, 𝑌〉} ∪ ∅) |
| 19 | | un0 4394 |
. . . . 5
⊢
({〈𝑋, 𝑌〉} ∪ ∅) =
{〈𝑋, 𝑌〉} |
| 20 | 18, 19 | eqtr2i 2766 |
. . . 4
⊢
{〈𝑋, 𝑌〉} = (∅ ∪
{〈𝑋, 𝑌〉}) |
| 21 | 16, 17, 20 | 3eqtr4g 2802 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ {𝑋}) = {〈𝑋, 𝑌〉}) |
| 22 | 21 | fveq1d 6908 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ {𝑋})‘𝑋) = ({〈𝑋, 𝑌〉}‘𝑋)) |
| 23 | | snidg 4660 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
| 24 | 23 | 3ad2ant1 1134 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → 𝑋 ∈ {𝑋}) |
| 25 | 24 | fvresd 6926 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ {𝑋})‘𝑋) = ((𝐹 ∪ {〈𝑋, 𝑌〉})‘𝑋)) |
| 26 | | fvsng 7200 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ({〈𝑋, 𝑌〉}‘𝑋) = 𝑌) |
| 27 | 26 | 3adant3 1133 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ({〈𝑋, 𝑌〉}‘𝑋) = 𝑌) |
| 28 | 22, 25, 27 | 3eqtr3d 2785 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {〈𝑋, 𝑌〉})‘𝑋) = 𝑌) |