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

Metamath Proof Explorer

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