Metamath Proof Explorer


Theorem upgrres

Description: A subgraph obtained by removing one vertex and all edges incident with this vertex from a pseudograph (see uhgrspan1 ) is a pseudograph. (Contributed by AV, 8-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 upgrres
|- ( ( G e. UPGraph /\ N e. V ) -> S e. UPGraph )

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 upgruhgr
 |-  ( G e. UPGraph -> 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. UPGraph -> Fun ( E |` F ) )
9 8 funfnd
 |-  ( G e. UPGraph -> ( E |` F ) Fn dom ( E |` F ) )
10 9 adantr
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( E |` F ) Fn dom ( E |` F ) )
11 1 2 3 upgrreslem
 |-  ( ( G e. UPGraph /\ 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. UPGraph /\ 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 isupgr
 |-  ( S e. _V -> ( S e. UPGraph <-> ( E |` F ) : dom ( E |` F ) --> { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
21 15 20 mp1i
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( S e. UPGraph <-> ( E |` F ) : dom ( E |` F ) --> { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
22 13 21 mpbird
 |-  ( ( G e. UPGraph /\ N e. V ) -> S e. UPGraph )