# 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 e. dom E | N e/ ( E ` i ) }`
upgrres.s
`|- S = <. ( V \ { N } ) , ( E |` F ) >.`
Assertion umgrres
`|- ( ( G e. UMGraph /\ N e. V ) -> S e. UMGraph )`

### Proof

Step Hyp Ref Expression
1 upgrres.v
` |-  V = ( Vtx ` G )`
2 upgrres.e
` |-  E = ( iEdg ` G )`
3 upgrres.f
` |-  F = { i e. dom E | N e/ ( E ` i ) }`
4 upgrres.s
` |-  S = <. ( V \ { N } ) , ( E |` F ) >.`
5 umgruhgr
` |-  ( G e. UMGraph -> G e. UHGraph )`
6 2 uhgrfun
` |-  ( G e. UHGraph -> Fun E )`
7 funres
` |-  ( Fun E -> Fun ( E |` F ) )`
8 5 6 7 3syl
` |-  ( G e. UMGraph -> Fun ( E |` F ) )`
9 8 funfnd
` |-  ( G e. UMGraph -> ( E |` F ) Fn dom ( E |` F ) )`
` |-  ( ( G e. UMGraph /\ N e. V ) -> ( E |` F ) Fn dom ( E |` F ) )`
11 1 2 3 umgrreslem
` |-  ( ( G e. UMGraph /\ N e. V ) -> ran ( E |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )`
12 df-f
` |-  ( ( E |` F ) : dom ( E |` F ) --> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } <-> ( ( E |` F ) Fn dom ( E |` F ) /\ ran ( E |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )`
13 10 11 12 sylanbrc
` |-  ( ( G e. UMGraph /\ N e. V ) -> ( E |` F ) : dom ( E |` F ) --> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )`
14 opex
` |-  <. ( V \ { N } ) , ( E |` F ) >. e. _V`
15 4 14 eqeltri
` |-  S e. _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 e. _V -> ( S e. UMGraph <-> ( E |` F ) : dom ( E |` F ) --> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )`
21 15 20 mp1i
` |-  ( ( G e. UMGraph /\ N e. V ) -> ( S e. UMGraph <-> ( E |` F ) : dom ( E |` F ) --> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )`
22 13 21 mpbird
` |-  ( ( G e. UMGraph /\ N e. V ) -> S e. UMGraph )`