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 )