Metamath Proof Explorer

Theorem fresunsn

Description: Recover the original function from a point-added function. See also funresdfunsn and fsnunres . (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Assertion fresunsn ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → F ↾ A ∖ X ∪ X Y = F

Proof

Step Hyp Ref Expression
1 fnrel ⊢ F Fn A → Rel ⁡ F
2 1 3ad2ant1 ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → Rel ⁡ F
3 resdmdfsn ⊢ Rel ⁡ F → F ↾ V ∖ X = F ↾ dom ⁡ F ∖ X
4 2 3 syl ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → F ↾ V ∖ X = F ↾ dom ⁡ F ∖ X
5 fndm ⊢ F Fn A → dom ⁡ F = A
6 5 3ad2ant1 ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → dom ⁡ F = A
7 6 difeq1d ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → dom ⁡ F ∖ X = A ∖ X
8 7 reseq2d ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → F ↾ dom ⁡ F ∖ X = F ↾ A ∖ X
9 4 8 eqtr2d ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → F ↾ A ∖ X = F ↾ V ∖ X
10 simp3 ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → F ⁡ X = Y
11 10 eqcomd ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → Y = F ⁡ X
12 11 opeq2d ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → X Y = X F ⁡ X
13 12 sneqd ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → X Y = X F ⁡ X
14 9 13 uneq12d ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → F ↾ A ∖ X ∪ X Y = F ↾ V ∖ X ∪ X F ⁡ X
15 fnfun ⊢ F Fn A → Fun ⁡ F
16 15 3ad2ant1 ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → Fun ⁡ F
17 5 eleq2d ⊢ F Fn A → X ∈ dom ⁡ F ↔ X ∈ A
18 17 biimpar ⊢ F Fn A ∧ X ∈ A → X ∈ dom ⁡ F
19 18 3adant3 ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → X ∈ dom ⁡ F
20 funresdfunsn ⊢ Fun ⁡ F ∧ X ∈ dom ⁡ F → F ↾ V ∖ X ∪ X F ⁡ X = F
21 16 19 20 syl2anc ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → F ↾ V ∖ X ∪ X F ⁡ X = F
22 14 21 eqtrd ⊢ F Fn A ∧ X ∈ A ∧ F ⁡ X = Y → F ↾ A ∖ X ∪ X Y = F