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