# 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 𝑉 = ( Vtx ‘ 𝐺 )
upgrres.e 𝐸 = ( iEdg ‘ 𝐺 )
upgrres.f 𝐹 = { 𝑖 ∈ dom 𝐸𝑁 ∉ ( 𝐸𝑖 ) }
upgrres.s 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐸𝐹 ) ⟩
Assertion umgrres ( ( 𝐺 ∈ UMGraph ∧ 𝑁𝑉 ) → 𝑆 ∈ UMGraph )

### Proof

Step Hyp Ref Expression
1 upgrres.v 𝑉 = ( Vtx ‘ 𝐺 )
2 upgrres.e 𝐸 = ( iEdg ‘ 𝐺 )
3 upgrres.f 𝐹 = { 𝑖 ∈ dom 𝐸𝑁 ∉ ( 𝐸𝑖 ) }
4 upgrres.s 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐸𝐹 ) ⟩
5 umgruhgr ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
6 2 uhgrfun ( 𝐺 ∈ UHGraph → Fun 𝐸 )
7 funres ( Fun 𝐸 → Fun ( 𝐸𝐹 ) )
8 5 6 7 3syl ( 𝐺 ∈ UMGraph → Fun ( 𝐸𝐹 ) )
9 8 funfnd ( 𝐺 ∈ UMGraph → ( 𝐸𝐹 ) Fn dom ( 𝐸𝐹 ) )
10 9 adantr ( ( 𝐺 ∈ UMGraph ∧ 𝑁𝑉 ) → ( 𝐸𝐹 ) Fn dom ( 𝐸𝐹 ) )
11 1 2 3 umgrreslem ( ( 𝐺 ∈ UMGraph ∧ 𝑁𝑉 ) → ran ( 𝐸𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
12 df-f ( ( 𝐸𝐹 ) : dom ( 𝐸𝐹 ) ⟶ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ↔ ( ( 𝐸𝐹 ) Fn dom ( 𝐸𝐹 ) ∧ ran ( 𝐸𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
13 10 11 12 sylanbrc ( ( 𝐺 ∈ UMGraph ∧ 𝑁𝑉 ) → ( 𝐸𝐹 ) : dom ( 𝐸𝐹 ) ⟶ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
14 opex ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐸𝐹 ) ⟩ ∈ V
15 4 14 eqeltri 𝑆 ∈ V
16 1 2 3 4 uhgrspan1lem2 ( Vtx ‘ 𝑆 ) = ( 𝑉 ∖ { 𝑁 } )
17 16 eqcomi ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 )
18 1 2 3 4 uhgrspan1lem3 ( iEdg ‘ 𝑆 ) = ( 𝐸𝐹 )
19 18 eqcomi ( 𝐸𝐹 ) = ( iEdg ‘ 𝑆 )
20 17 19 isumgrs ( 𝑆 ∈ V → ( 𝑆 ∈ UMGraph ↔ ( 𝐸𝐹 ) : dom ( 𝐸𝐹 ) ⟶ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
21 15 20 mp1i ( ( 𝐺 ∈ UMGraph ∧ 𝑁𝑉 ) → ( 𝑆 ∈ UMGraph ↔ ( 𝐸𝐹 ) : dom ( 𝐸𝐹 ) ⟶ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
22 13 21 mpbird ( ( 𝐺 ∈ UMGraph ∧ 𝑁𝑉 ) → 𝑆 ∈ UMGraph )