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

Metamath Proof Explorer

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 𝐹 → ( 𝐹 ↾ { 𝐵 } ) ⊆ { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )