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	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		resdmdfsn	⊢ ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) )
2		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
3	2	3ad2ant1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → dom 𝐹 = 𝐴 )
4	3	difeq1d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( dom 𝐹 ∖ { 𝑋 } ) = ( 𝐴 ∖ { 𝑋 } ) )
5	4	reseq2d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) )
6	1 5	eqtr2id	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) )
7		simp3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( 𝐹 ‘ 𝑋 ) = 𝑌 )
8	7	eqcomd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → 𝑌 = ( 𝐹 ‘ 𝑋 ) )
9	8	opeq2d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ )
10	9	sneqd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → { ⟨ 𝑋 , 𝑌 ⟩ } = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
11	6 10	uneq12d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) = ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
12		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
13	12	3ad2ant1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → Fun 𝐹 )
14	2	eleq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ 𝐴 ) )
15	14	biimpar	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ dom 𝐹 )
16	15	3adant3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → 𝑋 ∈ dom 𝐹 )
17		funresdfunsn	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) = 𝐹 )
18	13 16 17	syl2anc	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) = 𝐹 )
19	11 18	eqtrd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) = 𝐹 )