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

Metamath Proof Explorer

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