Theorem fsnunf

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

	Ref	Expression
Assertion	fsnunf	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝑆 ∪ { 𝑋 } ) ⟶ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → 𝐹 : 𝑆 ⟶ 𝑇 )
2		simp2l	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → 𝑋 ∈ 𝑉 )
3		simp3	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → 𝑌 ∈ 𝑇 )
4		f1osng	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑇 ) → { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } –1-1-onto→ { 𝑌 } )
5	2 3 4	syl2anc	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } –1-1-onto→ { 𝑌 } )
6		f1of	⊢ ( { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } –1-1-onto→ { 𝑌 } → { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } ⟶ { 𝑌 } )
7	5 6	syl	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } ⟶ { 𝑌 } )
8		simp2r	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ¬ 𝑋 ∈ 𝑆 )
9		disjsn	⊢ ( ( 𝑆 ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ 𝑆 )
10	8 9	sylibr	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ( 𝑆 ∩ { 𝑋 } ) = ∅ )
11		fun	⊢ ( ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ { ⟨ 𝑋 , 𝑌 ⟩ } : { 𝑋 } ⟶ { 𝑌 } ) ∧ ( 𝑆 ∩ { 𝑋 } ) = ∅ ) → ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝑆 ∪ { 𝑋 } ) ⟶ ( 𝑇 ∪ { 𝑌 } ) )
12	1 7 10 11	syl21anc	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝑆 ∪ { 𝑋 } ) ⟶ ( 𝑇 ∪ { 𝑌 } ) )
13		snssi	⊢ ( 𝑌 ∈ 𝑇 → { 𝑌 } ⊆ 𝑇 )
14	13	3ad2ant3	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → { 𝑌 } ⊆ 𝑇 )
15		ssequn2	⊢ ( { 𝑌 } ⊆ 𝑇 ↔ ( 𝑇 ∪ { 𝑌 } ) = 𝑇 )
16	14 15	sylib	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ( 𝑇 ∪ { 𝑌 } ) = 𝑇 )
17	16	feq3d	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝑆 ∪ { 𝑋 } ) ⟶ ( 𝑇 ∪ { 𝑌 } ) ↔ ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝑆 ∪ { 𝑋 } ) ⟶ 𝑇 ) )
18	12 17	mpbid	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : ( 𝑆 ∪ { 𝑋 } ) ⟶ 𝑇 )