Theorem funressn

Description: A function restricted to a singleton. (Contributed by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	funressn	⊢ ( Fun 𝐹 → ( 𝐹 ↾ { 𝐵 } ) ⊆ { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
2		fnressn	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
3	1 2	sylanb	⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
4		eqimss	⊢ ( ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } → ( 𝐹 ↾ { 𝐵 } ) ⊆ { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
5	3 4	syl	⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ( 𝐹 ↾ { 𝐵 } ) ⊆ { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
6		disjsn	⊢ ( ( dom 𝐹 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ dom 𝐹 )
7		fnresdisj	⊢ ( 𝐹 Fn dom 𝐹 → ( ( dom 𝐹 ∩ { 𝐵 } ) = ∅ ↔ ( 𝐹 ↾ { 𝐵 } ) = ∅ ) )
8	1 7	sylbi	⊢ ( Fun 𝐹 → ( ( dom 𝐹 ∩ { 𝐵 } ) = ∅ ↔ ( 𝐹 ↾ { 𝐵 } ) = ∅ ) )
9	6 8	bitr3id	⊢ ( Fun 𝐹 → ( ¬ 𝐵 ∈ dom 𝐹 ↔ ( 𝐹 ↾ { 𝐵 } ) = ∅ ) )
10	9	biimpa	⊢ ( ( Fun 𝐹 ∧ ¬ 𝐵 ∈ dom 𝐹 ) → ( 𝐹 ↾ { 𝐵 } ) = ∅ )
11		0ss	⊢ ∅ ⊆ { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ }
12	10 11	eqsstrdi	⊢ ( ( Fun 𝐹 ∧ ¬ 𝐵 ∈ dom 𝐹 ) → ( 𝐹 ↾ { 𝐵 } ) ⊆ { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
13	5 12	pm2.61dan	⊢ ( Fun 𝐹 → ( 𝐹 ↾ { 𝐵 } ) ⊆ { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )