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

Metamath Proof Explorer

Theorem fnressn

Description: A function restricted to a singleton. (Contributed by NM, 9-Oct-2004)

Ref Expression
Assertion fnressn ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )

Proof

Step Hyp Ref Expression
1 sneq ⊢ ( 𝑥 = 𝐵 → { 𝑥 } = { 𝐵 } )
2 1 reseq2d ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ↾ { 𝑥 } ) = ( 𝐹 ↾ { 𝐵 } ) )
3 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
4 opeq12 ⊢ ( ( 𝑥 = 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ = ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ )
5 3 4 mpdan ⊢ ( 𝑥 = 𝐵 → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ = ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ )
6 5 sneqd ⊢ ( 𝑥 = 𝐵 → { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
7 2 6 eqeq12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )
8 7 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) ↔ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) )
9 vex ⊢ 𝑥 ∈ V
10 9 snss ⊢ ( 𝑥 ∈ 𝐴 ↔ { 𝑥 } ⊆ 𝐴 )
11 fnssres ⊢ ( ( 𝐹 Fn 𝐴 ∧ { 𝑥 } ⊆ 𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } )
12 10 11 sylan2b ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } )
13 dffn2 ⊢ ( ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } ↔ ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ V )
14 9 fsn2 ⊢ ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ V ↔ ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ) )
15 fvex ⊢ ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V
16 15 biantrur ⊢ ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ↔ ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ) )
17 vsnid ⊢ 𝑥 ∈ { 𝑥 }
18 fvres ⊢ ( 𝑥 ∈ { 𝑥 } → ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
19 17 18 ax-mp ⊢ ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 )
20 19 opeq2i ⊢ ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩
21 20 sneqi ⊢ { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ }
22 21 eqeq2i ⊢ ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ↔ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
23 16 22 bitr3i ⊢ ( ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ) ↔ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
24 13 14 23 3bitri ⊢ ( ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } ↔ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
25 12 24 sylib ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
26 25 expcom ⊢ ( 𝑥 ∈ 𝐴 → ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) )
27 8 26 vtoclga ⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )
28 27 impcom ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )