Metamath Proof Explorer

Theorem fnressn

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

Ref Expression
Assertion fnressn ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to {{F}↾}_{\left\{{B}\right\}}=\left\{⟨{B},{F}\left({B}\right)⟩\right\}$

Proof

Step Hyp Ref Expression
1 sneq ${⊢}{x}={B}\to \left\{{x}\right\}=\left\{{B}\right\}$
2 1 reseq2d ${⊢}{x}={B}\to {{F}↾}_{\left\{{x}\right\}}={{F}↾}_{\left\{{B}\right\}}$
3 fveq2 ${⊢}{x}={B}\to {F}\left({x}\right)={F}\left({B}\right)$
4 opeq12 ${⊢}\left({x}={B}\wedge {F}\left({x}\right)={F}\left({B}\right)\right)\to ⟨{x},{F}\left({x}\right)⟩=⟨{B},{F}\left({B}\right)⟩$
5 3 4 mpdan ${⊢}{x}={B}\to ⟨{x},{F}\left({x}\right)⟩=⟨{B},{F}\left({B}\right)⟩$
6 5 sneqd ${⊢}{x}={B}\to \left\{⟨{x},{F}\left({x}\right)⟩\right\}=\left\{⟨{B},{F}\left({B}\right)⟩\right\}$
7 2 6 eqeq12d ${⊢}{x}={B}\to \left({{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},{F}\left({x}\right)⟩\right\}↔{{F}↾}_{\left\{{B}\right\}}=\left\{⟨{B},{F}\left({B}\right)⟩\right\}\right)$
8 7 imbi2d ${⊢}{x}={B}\to \left(\left({F}Fn{A}\to {{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},{F}\left({x}\right)⟩\right\}\right)↔\left({F}Fn{A}\to {{F}↾}_{\left\{{B}\right\}}=\left\{⟨{B},{F}\left({B}\right)⟩\right\}\right)\right)$
9 vex ${⊢}{x}\in \mathrm{V}$
10 9 snss ${⊢}{x}\in {A}↔\left\{{x}\right\}\subseteq {A}$
11 fnssres ${⊢}\left({F}Fn{A}\wedge \left\{{x}\right\}\subseteq {A}\right)\to \left({{F}↾}_{\left\{{x}\right\}}\right)Fn\left\{{x}\right\}$
12 10 11 sylan2b ${⊢}\left({F}Fn{A}\wedge {x}\in {A}\right)\to \left({{F}↾}_{\left\{{x}\right\}}\right)Fn\left\{{x}\right\}$
13 dffn2 ${⊢}\left({{F}↾}_{\left\{{x}\right\}}\right)Fn\left\{{x}\right\}↔\left({{F}↾}_{\left\{{x}\right\}}\right):\left\{{x}\right\}⟶\mathrm{V}$
14 9 fsn2 ${⊢}\left({{F}↾}_{\left\{{x}\right\}}\right):\left\{{x}\right\}⟶\mathrm{V}↔\left(\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)\in \mathrm{V}\wedge {{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)⟩\right\}\right)$
15 fvex ${⊢}\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)\in \mathrm{V}$
16 15 biantrur ${⊢}{{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)⟩\right\}↔\left(\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)\in \mathrm{V}\wedge {{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)⟩\right\}\right)$
17 vsnid ${⊢}{x}\in \left\{{x}\right\}$
18 fvres ${⊢}{x}\in \left\{{x}\right\}\to \left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)={F}\left({x}\right)$
19 17 18 ax-mp ${⊢}\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)={F}\left({x}\right)$
20 19 opeq2i ${⊢}⟨{x},\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)⟩=⟨{x},{F}\left({x}\right)⟩$
21 20 sneqi ${⊢}\left\{⟨{x},\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)⟩\right\}=\left\{⟨{x},{F}\left({x}\right)⟩\right\}$
22 21 eqeq2i ${⊢}{{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)⟩\right\}↔{{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},{F}\left({x}\right)⟩\right\}$
23 16 22 bitr3i ${⊢}\left(\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)\in \mathrm{V}\wedge {{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},\left({{F}↾}_{\left\{{x}\right\}}\right)\left({x}\right)⟩\right\}\right)↔{{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},{F}\left({x}\right)⟩\right\}$
24 13 14 23 3bitri ${⊢}\left({{F}↾}_{\left\{{x}\right\}}\right)Fn\left\{{x}\right\}↔{{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},{F}\left({x}\right)⟩\right\}$
25 12 24 sylib ${⊢}\left({F}Fn{A}\wedge {x}\in {A}\right)\to {{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},{F}\left({x}\right)⟩\right\}$
26 25 expcom ${⊢}{x}\in {A}\to \left({F}Fn{A}\to {{F}↾}_{\left\{{x}\right\}}=\left\{⟨{x},{F}\left({x}\right)⟩\right\}\right)$
27 8 26 vtoclga ${⊢}{B}\in {A}\to \left({F}Fn{A}\to {{F}↾}_{\left\{{B}\right\}}=\left\{⟨{B},{F}\left({B}\right)⟩\right\}\right)$
28 27 impcom ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to {{F}↾}_{\left\{{B}\right\}}=\left\{⟨{B},{F}\left({B}\right)⟩\right\}$