Metamath Proof Explorer

Theorem umgrres

Description: A subgraph obtained by removing one vertex and all edges incident with this vertex from a multigraph (see uhgrspan1 ) is a multigraph. (Contributed by AV, 27-Nov-2020) (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 umgrres ⊢G∈UMGraph∧N∈V→S∈UMGraph

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 umgruhgr ⊢G∈UMGraph→G∈UHGraph
6 2 uhgrfun ⊢G∈UHGraph→Fun⁡E
7 funres ⊢Fun⁡E→Fun⁡E↾F
8 5 6 7 3syl ⊢G∈UMGraph→Fun⁡E↾F
9 8 funfnd ⊢G∈UMGraph→E↾FFndom⁡E↾F
10 9 adantr ⊢G∈UMGraph∧N∈V→E↾FFndom⁡E↾F
11 1 2 3 umgrreslem ⊢G∈UMGraph∧N∈V→ran⁡E↾F⊆p∈𝒫V∖N|p=2
12 df-f ⊢E↾F:dom⁡E↾F⟶p∈𝒫V∖N|p=2↔E↾FFndom⁡E↾F∧ran⁡E↾F⊆p∈𝒫V∖N|p=2
13 10 11 12 sylanbrc ⊢G∈UMGraph∧N∈V→E↾F:dom⁡E↾F⟶p∈𝒫V∖N|p=2
14 opex ⊢V∖NE↾F∈V
15 4 14 eqeltri ⊢S∈V
16 1 2 3 4 uhgrspan1lem2 ⊢Vtx⁡S=V∖N
17 16 eqcomi ⊢V∖N=Vtx⁡S
18 1 2 3 4 uhgrspan1lem3 ⊢iEdg⁡S=E↾F
19 18 eqcomi ⊢E↾F=iEdg⁡S
20 17 19 isumgrs ⊢S∈V→S∈UMGraph↔E↾F:dom⁡E↾F⟶p∈𝒫V∖N|p=2
21 15 20 mp1i ⊢G∈UMGraph∧N∈V→S∈UMGraph↔E↾F:dom⁡E↾F⟶p∈𝒫V∖N|p=2
22 13 21 mpbird ⊢G∈UMGraph∧N∈V→S∈UMGraph