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

Metamath Proof Explorer

Theorem fsnunf2

Description: Adjoining a point to a punctured function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Assertion fsnunf2 ( ( 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇 ) → ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : 𝑆 ⟶ 𝑇 )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇 ) → 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 )
2 simp2 ⊢ ( ( 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇 ) → 𝑋 ∈ 𝑆 )
3 neldifsnd ⊢ ( ( 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇 ) → ¬ 𝑋 ∈ ( 𝑆 ∖ { 𝑋 } ) )
4 simp3 ⊢ ( ( 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇 ) → 𝑌 ∈ 𝑇 )
5 fsnunf ⊢ ( ( 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑆 ∧ ¬ 𝑋 ∈ ( 𝑆 ∖ { 𝑋 } ) ) ∧ 𝑌 ∈ 𝑇 ) → ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( ( 𝑆 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ⟶ 𝑇 )
6 1 2 3 4 5 syl121anc ⊢ ( ( 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇 ) → ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( ( 𝑆 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ⟶ 𝑇 )
7 difsnid ⊢ ( 𝑋 ∈ 𝑆 → ( ( 𝑆 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = 𝑆 )
8 7 3ad2ant2 ⊢ ( ( 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇 ) → ( ( 𝑆 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = 𝑆 )
9 8 feq2d ⊢ ( ( 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇 ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( ( 𝑆 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ⟶ 𝑇 ↔ ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : 𝑆 ⟶ 𝑇 ) )
10 6 9 mpbid ⊢ ( ( 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇 ) → ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : 𝑆 ⟶ 𝑇 )