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=Vtx⁡G
upgrres.e ⊢E=iEdg⁡G
upgrres.f ⊢F=i∈dom⁡E|N∉E⁡i
upgrres.s ⊢S=V∖NE↾F
Assertion usgrres ⊢G∈USGraph∧N∈V→S∈USGraph

Proof

Step Hyp Ref Expression
1 upgrres.v ⊢V=Vtx⁡G
2 upgrres.e ⊢E=iEdg⁡G
3 upgrres.f ⊢F=i∈dom⁡E|N∉E⁡i
4 upgrres.s ⊢S=V∖NE↾F
5 1 2 usgrf ⊢G∈USGraph→E:dom⁡E⟶1-1x∈𝒫V∖∅|x=2
6 3 ssrab3 ⊢F⊆dom⁡E
7 6 a1i ⊢G∈USGraph∧N∈V→F⊆dom⁡E
8 f1ssres ⊢E:dom⁡E⟶1-1x∈𝒫V∖∅|x=2∧F⊆dom⁡E→E↾F:F⟶1-1x∈𝒫V∖∅|x=2
9 5 7 8 syl2an2r ⊢G∈USGraph∧N∈V→E↾F:F⟶1-1x∈𝒫V∖∅|x=2
10 usgrumgr ⊢G∈USGraph→G∈UMGraph
11 1 2 3 umgrreslem ⊢G∈UMGraph∧N∈V→ran⁡E↾F⊆p∈𝒫V∖N|p=2
12 10 11 sylan ⊢G∈USGraph∧N∈V→ran⁡E↾F⊆p∈𝒫V∖N|p=2
13 f1ssr ⊢E↾F:F⟶1-1x∈𝒫V∖∅|x=2∧ran⁡E↾F⊆p∈𝒫V∖N|p=2→E↾F:F⟶1-1p∈𝒫V∖N|p=2
14 9 12 13 syl2anc ⊢G∈USGraph∧N∈V→E↾F:F⟶1-1p∈𝒫V∖N|p=2
15 ssdmres ⊢F⊆dom⁡E↔dom⁡E↾F=F
16 6 15 mpbi ⊢dom⁡E↾F=F
17 f1eq2 ⊢dom⁡E↾F=F→E↾F:dom⁡E↾F⟶1-1p∈𝒫V∖N|p=2↔E↾F:F⟶1-1p∈𝒫V∖N|p=2
18 16 17 ax-mp ⊢E↾F:dom⁡E↾F⟶1-1p∈𝒫V∖N|p=2↔E↾F:F⟶1-1p∈𝒫V∖N|p=2
19 14 18 sylibr ⊢G∈USGraph∧N∈V→E↾F:dom⁡E↾F⟶1-1p∈𝒫V∖N|p=2
20 opex ⊢V∖NE↾F∈V
21 4 20 eqeltri ⊢S∈V
22 1 2 3 4 uhgrspan1lem2 ⊢Vtx⁡S=V∖N
23 22 eqcomi ⊢V∖N=Vtx⁡S
24 1 2 3 4 uhgrspan1lem3 ⊢iEdg⁡S=E↾F
25 24 eqcomi ⊢E↾F=iEdg⁡S
26 23 25 isusgrs ⊢S∈V→S∈USGraph↔E↾F:dom⁡E↾F⟶1-1p∈𝒫V∖N|p=2
27 21 26 mp1i ⊢G∈USGraph∧N∈V→S∈USGraph↔E↾F:dom⁡E↾F⟶1-1p∈𝒫V∖N|p=2
28 19 27 mpbird ⊢G∈USGraph∧N∈V→S∈USGraph