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

Metamath Proof Explorer

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