Metamath Proof Explorer

Theorem upgrres

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

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 upgruhgr ⊢G∈UPGraph→G∈UHGraph
6 2 uhgrfun ⊢G∈UHGraph→Fun⁡E
7 funres ⊢Fun⁡E→Fun⁡E↾F
8 5 6 7 3syl ⊢G∈UPGraph→Fun⁡E↾F
9 8 funfnd ⊢G∈UPGraph→E↾FFndom⁡E↾F
10 9 adantr ⊢G∈UPGraph∧N∈V→E↾FFndom⁡E↾F
11 1 2 3 upgrreslem ⊢G∈UPGraph∧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∈UPGraph∧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 isupgr ⊢S∈V→S∈UPGraph↔E↾F:dom⁡E↾F⟶p∈𝒫V∖N∖∅|p≤2
21 15 20 mp1i ⊢G∈UPGraph∧N∈V→S∈UPGraph↔E↾F:dom⁡E↾F⟶p∈𝒫V∖N∖∅|p≤2
22 13 21 mpbird ⊢G∈UPGraph∧N∈V→S∈UPGraph