This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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