Theorem umgrres1

Description: A multigraph obtained by removing one vertex and all edges incident with this vertex is a multigraph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr since the domains of the edge functions may not be compatible. (Contributed by AV, 27-Nov-2020)

	Ref	Expression
Hypotheses	upgrres1.v	|- V = ( Vtx ` G )
	upgrres1.e	|- E = ( Edg ` G )
	upgrres1.f	|- F = { e e. E | N e/ e }
	upgrres1.s	|- S = <. ( V \ { N } ) , ( _I |` F ) >.
Assertion	umgrres1	|- ( ( G e. UMGraph /\ N e. V ) -> S e. UMGraph )

Proof

Step	Hyp	Ref	Expression
1		upgrres1.v	|- V = ( Vtx ` G )
2		upgrres1.e	|- E = ( Edg ` G )
3		upgrres1.f	|- F = { e e. E | N e/ e }
4		upgrres1.s	|- S = <. ( V \ { N } ) , ( _I |` F ) >.
5		f1oi	|- ( _I |` F ) : F -1-1-onto-> F
6		f1of	|- ( ( _I |` F ) : F -1-1-onto-> F -> ( _I |` F ) : F --> F )
7	5 6	mp1i	|- ( ( G e. UMGraph /\ N e. V ) -> ( _I |` F ) : F --> F )
8	7	ffdmd	|- ( ( G e. UMGraph /\ N e. V ) -> ( _I |` F ) : dom ( _I |` F ) --> F )
9		rnresi	|- ran ( _I |` F ) = F
10	1 2 3	umgrres1lem	|- ( ( G e. UMGraph /\ N e. V ) -> ran ( _I |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
11	9 10	eqsstrrid	|- ( ( G e. UMGraph /\ N e. V ) -> F C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
12	8 11	fssd	|- ( ( G e. UMGraph /\ N e. V ) -> ( _I |` F ) : dom ( _I |` F ) --> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
13		opex	|- <. ( V \ { N } ) , ( _I |` F ) >. e. _V
14	4 13	eqeltri	|- S e. _V
15	1 2 3 4	upgrres1lem2	|- ( Vtx ` S ) = ( V \ { N } )
16	15	eqcomi	|- ( V \ { N } ) = ( Vtx ` S )
17	1 2 3 4	upgrres1lem3	|- ( iEdg ` S ) = ( _I |` F )
18	17	eqcomi	|- ( _I |` F ) = ( iEdg ` S )
19	16 18	isumgrs	|- ( S e. _V -> ( S e. UMGraph <-> ( _I |` F ) : dom ( _I |` F ) --> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )
20	14 19	mp1i	|- ( ( G e. UMGraph /\ N e. V ) -> ( S e. UMGraph <-> ( _I |` F ) : dom ( _I |` F ) --> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )
21	12 20	mpbird	|- ( ( G e. UMGraph /\ N e. V ) -> S e. UMGraph )