# Metamath Proof Explorer

## Theorem usgrres

Description: A subgraph obtained by removing one vertex and all edges incident with this vertex from a simple graph (see uhgrspan1 ) is a simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 19-Dec-2021)

Ref Expression
Hypotheses upgrres.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
upgrres.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
upgrres.f ${⊢}{F}=\left\{{i}\in \mathrm{dom}{E}|{N}\notin {E}\left({i}\right)\right\}$
upgrres.s ${⊢}{S}=⟨{V}\setminus \left\{{N}\right\},{{E}↾}_{{F}}⟩$
Assertion usgrres ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to {S}\in \mathrm{USGraph}$

### Proof

Step Hyp Ref Expression
1 upgrres.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 upgrres.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
3 upgrres.f ${⊢}{F}=\left\{{i}\in \mathrm{dom}{E}|{N}\notin {E}\left({i}\right)\right\}$
4 upgrres.s ${⊢}{S}=⟨{V}\setminus \left\{{N}\right\},{{E}↾}_{{F}}⟩$
5 1 2 usgrf ${⊢}{G}\in \mathrm{USGraph}\to {E}:\mathrm{dom}{E}\underset{1-1}{⟶}\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}$
6 3 ssrab3 ${⊢}{F}\subseteq \mathrm{dom}{E}$
7 6 a1i ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to {F}\subseteq \mathrm{dom}{E}$
8 f1ssres ${⊢}\left({E}:\mathrm{dom}{E}\underset{1-1}{⟶}\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}\wedge {F}\subseteq \mathrm{dom}{E}\right)\to \left({{E}↾}_{{F}}\right):{F}\underset{1-1}{⟶}\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}$
9 5 7 8 syl2an2r ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to \left({{E}↾}_{{F}}\right):{F}\underset{1-1}{⟶}\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}$
10 usgrumgr ${⊢}{G}\in \mathrm{USGraph}\to {G}\in \mathrm{UMGraph}$
11 1 2 3 umgrreslem ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \mathrm{ran}\left({{E}↾}_{{F}}\right)\subseteq \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$
12 10 11 sylan ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to \mathrm{ran}\left({{E}↾}_{{F}}\right)\subseteq \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$
13 f1ssr ${⊢}\left(\left({{E}↾}_{{F}}\right):{F}\underset{1-1}{⟶}\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}\wedge \mathrm{ran}\left({{E}↾}_{{F}}\right)\subseteq \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)\to \left({{E}↾}_{{F}}\right):{F}\underset{1-1}{⟶}\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$
14 9 12 13 syl2anc ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to \left({{E}↾}_{{F}}\right):{F}\underset{1-1}{⟶}\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$
15 ssdmres ${⊢}{F}\subseteq \mathrm{dom}{E}↔\mathrm{dom}\left({{E}↾}_{{F}}\right)={F}$
16 6 15 mpbi ${⊢}\mathrm{dom}\left({{E}↾}_{{F}}\right)={F}$
17 f1eq2 ${⊢}\mathrm{dom}\left({{E}↾}_{{F}}\right)={F}\to \left(\left({{E}↾}_{{F}}\right):\mathrm{dom}\left({{E}↾}_{{F}}\right)\underset{1-1}{⟶}\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}↔\left({{E}↾}_{{F}}\right):{F}\underset{1-1}{⟶}\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)$
18 16 17 ax-mp ${⊢}\left({{E}↾}_{{F}}\right):\mathrm{dom}\left({{E}↾}_{{F}}\right)\underset{1-1}{⟶}\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}↔\left({{E}↾}_{{F}}\right):{F}\underset{1-1}{⟶}\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$
19 14 18 sylibr ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to \left({{E}↾}_{{F}}\right):\mathrm{dom}\left({{E}↾}_{{F}}\right)\underset{1-1}{⟶}\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$
20 opex ${⊢}⟨{V}\setminus \left\{{N}\right\},{{E}↾}_{{F}}⟩\in \mathrm{V}$
21 4 20 eqeltri ${⊢}{S}\in \mathrm{V}$
22 1 2 3 4 uhgrspan1lem2 ${⊢}\mathrm{Vtx}\left({S}\right)={V}\setminus \left\{{N}\right\}$
23 22 eqcomi ${⊢}{V}\setminus \left\{{N}\right\}=\mathrm{Vtx}\left({S}\right)$
24 1 2 3 4 uhgrspan1lem3 ${⊢}\mathrm{iEdg}\left({S}\right)={{E}↾}_{{F}}$
25 24 eqcomi ${⊢}{{E}↾}_{{F}}=\mathrm{iEdg}\left({S}\right)$
26 23 25 isusgrs ${⊢}{S}\in \mathrm{V}\to \left({S}\in \mathrm{USGraph}↔\left({{E}↾}_{{F}}\right):\mathrm{dom}\left({{E}↾}_{{F}}\right)\underset{1-1}{⟶}\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)$
27 21 26 mp1i ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to \left({S}\in \mathrm{USGraph}↔\left({{E}↾}_{{F}}\right):\mathrm{dom}\left({{E}↾}_{{F}}\right)\underset{1-1}{⟶}\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)$
28 19 27 mpbird ${⊢}\left({G}\in \mathrm{USGraph}\wedge {N}\in {V}\right)\to {S}\in \mathrm{USGraph}$