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 ) )
10 9 adantr 
 |-  ( ( 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 )