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

### 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 1 2 usgrf
` |-  ( G e. USGraph -> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } )`
6 3 ssrab3
` |-  F C_ dom E`
7 6 a1i
` |-  ( ( G e. USGraph /\ N e. V ) -> F C_ dom E )`
8 f1ssres
` |-  ( ( E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } /\ F C_ dom E ) -> ( E |` F ) : F -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } )`
9 5 7 8 syl2an2r
` |-  ( ( G e. USGraph /\ N e. V ) -> ( E |` F ) : F -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } )`
10 usgrumgr
` |-  ( G e. USGraph -> G e. UMGraph )`
11 1 2 3 umgrreslem
` |-  ( ( G e. UMGraph /\ N e. V ) -> ran ( E |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )`
12 10 11 sylan
` |-  ( ( G e. USGraph /\ N e. V ) -> ran ( E |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )`
13 f1ssr
` |-  ( ( ( E |` F ) : F -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } /\ ran ( E |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) -> ( E |` F ) : F -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )`
14 9 12 13 syl2anc
` |-  ( ( G e. USGraph /\ N e. V ) -> ( E |` F ) : F -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )`
15 ssdmres
` |-  ( F C_ 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-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } <-> ( E |` F ) : F -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )`
18 16 17 ax-mp
` |-  ( ( E |` F ) : dom ( E |` F ) -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } <-> ( E |` F ) : F -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )`
19 14 18 sylibr
` |-  ( ( G e. USGraph /\ N e. V ) -> ( E |` F ) : dom ( E |` F ) -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )`
20 opex
` |-  <. ( V \ { N } ) , ( E |` F ) >. e. _V`
21 4 20 eqeltri
` |-  S e. _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 e. _V -> ( S e. USGraph <-> ( E |` F ) : dom ( E |` F ) -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )`
27 21 26 mp1i
` |-  ( ( G e. USGraph /\ N e. V ) -> ( S e. USGraph <-> ( E |` F ) : dom ( E |` F ) -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )`
28 19 27 mpbird
` |-  ( ( G e. USGraph /\ N e. V ) -> S e. USGraph )`