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	⊢ ( ( 𝐹 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇 ) → ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : 𝑆 ⟶ 𝑇 )