Theorem fsnunres

Description: Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015)

	Ref	Expression
Assertion	fsnunres	⊢ ( ( 𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆 ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ↾ 𝑆 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fnresdm	⊢ ( 𝐹 Fn 𝑆 → ( 𝐹 ↾ 𝑆 ) = 𝐹 )
2	1	adantr	⊢ ( ( 𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆 ) → ( 𝐹 ↾ 𝑆 ) = 𝐹 )
3		ressnop0	⊢ ( ¬ 𝑋 ∈ 𝑆 → ( { ⟨ 𝑋 , 𝑌 ⟩ } ↾ 𝑆 ) = ∅ )
4	3	adantl	⊢ ( ( 𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆 ) → ( { ⟨ 𝑋 , 𝑌 ⟩ } ↾ 𝑆 ) = ∅ )
5	2 4	uneq12d	⊢ ( ( 𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆 ) → ( ( 𝐹 ↾ 𝑆 ) ∪ ( { ⟨ 𝑋 , 𝑌 ⟩ } ↾ 𝑆 ) ) = ( 𝐹 ∪ ∅ ) )
6		resundir	⊢ ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ↾ 𝑆 ) = ( ( 𝐹 ↾ 𝑆 ) ∪ ( { ⟨ 𝑋 , 𝑌 ⟩ } ↾ 𝑆 ) )
7		un0	⊢ ( 𝐹 ∪ ∅ ) = 𝐹
8	7	eqcomi	⊢ 𝐹 = ( 𝐹 ∪ ∅ )
9	5 6 8	3eqtr4g	⊢ ( ( 𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆 ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ↾ 𝑆 ) = 𝐹 )