Metamath Proof Explorer

Theorem fsnunfv

Description: Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by NM, 18-May-2017)

Ref Expression
Assertion fsnunfv ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to \left({F}\cup \left\{⟨{X},{Y}⟩\right\}\right)\left({X}\right)={Y}$

Proof

Step Hyp Ref Expression
1 dmres ${⊢}\mathrm{dom}\left({{F}↾}_{\left\{{X}\right\}}\right)=\left\{{X}\right\}\cap \mathrm{dom}{F}$
2 incom ${⊢}\left\{{X}\right\}\cap \mathrm{dom}{F}=\mathrm{dom}{F}\cap \left\{{X}\right\}$
3 1 2 eqtri ${⊢}\mathrm{dom}\left({{F}↾}_{\left\{{X}\right\}}\right)=\mathrm{dom}{F}\cap \left\{{X}\right\}$
4 disjsn ${⊢}\mathrm{dom}{F}\cap \left\{{X}\right\}=\varnothing ↔¬{X}\in \mathrm{dom}{F}$
5 4 biimpri ${⊢}¬{X}\in \mathrm{dom}{F}\to \mathrm{dom}{F}\cap \left\{{X}\right\}=\varnothing$
6 3 5 syl5eq ${⊢}¬{X}\in \mathrm{dom}{F}\to \mathrm{dom}\left({{F}↾}_{\left\{{X}\right\}}\right)=\varnothing$
7 6 3ad2ant3 ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to \mathrm{dom}\left({{F}↾}_{\left\{{X}\right\}}\right)=\varnothing$
8 relres ${⊢}\mathrm{Rel}\left({{F}↾}_{\left\{{X}\right\}}\right)$
9 reldm0 ${⊢}\mathrm{Rel}\left({{F}↾}_{\left\{{X}\right\}}\right)\to \left({{F}↾}_{\left\{{X}\right\}}=\varnothing ↔\mathrm{dom}\left({{F}↾}_{\left\{{X}\right\}}\right)=\varnothing \right)$
10 8 9 ax-mp ${⊢}{{F}↾}_{\left\{{X}\right\}}=\varnothing ↔\mathrm{dom}\left({{F}↾}_{\left\{{X}\right\}}\right)=\varnothing$
11 7 10 sylibr ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to {{F}↾}_{\left\{{X}\right\}}=\varnothing$
12 fnsng ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\right)\to \left\{⟨{X},{Y}⟩\right\}Fn\left\{{X}\right\}$
13 12 3adant3 ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to \left\{⟨{X},{Y}⟩\right\}Fn\left\{{X}\right\}$
14 fnresdm ${⊢}\left\{⟨{X},{Y}⟩\right\}Fn\left\{{X}\right\}\to {\left\{⟨{X},{Y}⟩\right\}↾}_{\left\{{X}\right\}}=\left\{⟨{X},{Y}⟩\right\}$
15 13 14 syl ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to {\left\{⟨{X},{Y}⟩\right\}↾}_{\left\{{X}\right\}}=\left\{⟨{X},{Y}⟩\right\}$
16 11 15 uneq12d ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to \left({{F}↾}_{\left\{{X}\right\}}\right)\cup \left({\left\{⟨{X},{Y}⟩\right\}↾}_{\left\{{X}\right\}}\right)=\varnothing \cup \left\{⟨{X},{Y}⟩\right\}$
17 resundir ${⊢}{\left({F}\cup \left\{⟨{X},{Y}⟩\right\}\right)↾}_{\left\{{X}\right\}}=\left({{F}↾}_{\left\{{X}\right\}}\right)\cup \left({\left\{⟨{X},{Y}⟩\right\}↾}_{\left\{{X}\right\}}\right)$
18 uncom ${⊢}\varnothing \cup \left\{⟨{X},{Y}⟩\right\}=\left\{⟨{X},{Y}⟩\right\}\cup \varnothing$
19 un0 ${⊢}\left\{⟨{X},{Y}⟩\right\}\cup \varnothing =\left\{⟨{X},{Y}⟩\right\}$
20 18 19 eqtr2i ${⊢}\left\{⟨{X},{Y}⟩\right\}=\varnothing \cup \left\{⟨{X},{Y}⟩\right\}$
21 16 17 20 3eqtr4g ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to {\left({F}\cup \left\{⟨{X},{Y}⟩\right\}\right)↾}_{\left\{{X}\right\}}=\left\{⟨{X},{Y}⟩\right\}$
22 21 fveq1d ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to \left({\left({F}\cup \left\{⟨{X},{Y}⟩\right\}\right)↾}_{\left\{{X}\right\}}\right)\left({X}\right)=\left\{⟨{X},{Y}⟩\right\}\left({X}\right)$
23 snidg ${⊢}{X}\in {V}\to {X}\in \left\{{X}\right\}$
24 23 3ad2ant1 ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to {X}\in \left\{{X}\right\}$
25 24 fvresd ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to \left({\left({F}\cup \left\{⟨{X},{Y}⟩\right\}\right)↾}_{\left\{{X}\right\}}\right)\left({X}\right)=\left({F}\cup \left\{⟨{X},{Y}⟩\right\}\right)\left({X}\right)$
26 fvsng ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\right)\to \left\{⟨{X},{Y}⟩\right\}\left({X}\right)={Y}$
27 26 3adant3 ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to \left\{⟨{X},{Y}⟩\right\}\left({X}\right)={Y}$
28 22 25 27 3eqtr3d ${⊢}\left({X}\in {V}\wedge {Y}\in {W}\wedge ¬{X}\in \mathrm{dom}{F}\right)\to \left({F}\cup \left\{⟨{X},{Y}⟩\right\}\right)\left({X}\right)={Y}$