Theorem funresdfunsn

Description: Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in the function itself. (Contributed by AV, 2-Dec-2018)

	Ref	Expression
Assertion	funresdfunsn	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
2		resdmdfsn	⊢ ( Rel 𝐹 → ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) )
3	1 2	syl	⊢ ( Fun 𝐹 → ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) )
4	3	adantr	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) )
5	4	uneq1d	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) = ( ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
6		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
7		fnsnsplit	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → 𝐹 = ( ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
8	6 7	sylanb	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → 𝐹 = ( ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
9	5 8	eqtr4d	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) = 𝐹 )