Theorem fnsnsplit

Description: Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015)

	Ref	Expression
Assertion	fnsnsplit	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐹 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		fnresdm	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
2	1	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
3		resundi	⊢ ( 𝐹 ↾ ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ ( 𝐹 ↾ { 𝑋 } ) )
4		difsnid	⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = 𝐴 )
5	4	adantl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = 𝐴 )
6	5	reseq2d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ↾ ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = ( 𝐹 ↾ 𝐴 ) )
7		fnressn	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝑋 } ) = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } )
8	7	uneq2d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ ( 𝐹 ↾ { 𝑋 } ) ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
9	3 6 8	3eqtr3a	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ↾ 𝐴 ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )
10	2 9	eqtr3d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐹 = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) )