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