Theorem usgrres1

Description: Restricting a simple graph by removing one vertex results in a simple graph. Remark: This restricted 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 Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 10-Jan-2020) (Revised by AV, 23-Oct-2020) (Proof shortened 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	usgrres1	|- ( ( G e. USGraph /\ N e. V ) -> S e. USGraph )

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		f1of1	|- ( ( _I |` F ) : F -1-1-onto-> F -> ( _I |` F ) : F -1-1-> F )
7	5 6	mp1i	|- ( ( G e. USGraph /\ N e. V ) -> ( _I |` F ) : F -1-1-> F )
8		eqidd	|- ( ( G e. USGraph /\ N e. V ) -> ( _I |` F ) = ( _I |` F ) )
9		dmresi	|- dom ( _I |` F ) = F
10	9	a1i	|- ( ( G e. USGraph /\ N e. V ) -> dom ( _I |` F ) = F )
11		eqidd	|- ( ( G e. USGraph /\ N e. V ) -> F = F )
12	8 10 11	f1eq123d	|- ( ( G e. USGraph /\ N e. V ) -> ( ( _I |` F ) : dom ( _I |` F ) -1-1-> F <-> ( _I |` F ) : F -1-1-> F ) )
13	7 12	mpbird	|- ( ( G e. USGraph /\ N e. V ) -> ( _I |` F ) : dom ( _I |` F ) -1-1-> F )
14		usgrumgr	|- ( G e. USGraph -> G e. UMGraph )
15	1 2 3	umgrres1lem	|- ( ( G e. UMGraph /\ N e. V ) -> ran ( _I |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
16	14 15	sylan	|- ( ( G e. USGraph /\ N e. V ) -> ran ( _I |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
17		f1ssr	|- ( ( ( _I |` F ) : dom ( _I |` F ) -1-1-> F /\ ran ( _I |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) -> ( _I |` F ) : dom ( _I |` F ) -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
18	13 16 17	syl2anc	|- ( ( G e. USGraph /\ N e. V ) -> ( _I |` F ) : dom ( _I |` F ) -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
19		opex	|- <. ( V \ { N } ) , ( _I |` F ) >. e. _V
20	4 19	eqeltri	|- S e. _V
21	1 2 3 4	upgrres1lem2	|- ( Vtx ` S ) = ( V \ { N } )
22	21	eqcomi	|- ( V \ { N } ) = ( Vtx ` S )
23	1 2 3 4	upgrres1lem3	|- ( iEdg ` S ) = ( _I |` F )
24	23	eqcomi	|- ( _I |` F ) = ( iEdg ` S )
25	22 24	isusgrs	|- ( S e. _V -> ( S e. USGraph <-> ( _I |` F ) : dom ( _I |` F ) -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )
26	20 25	mp1i	|- ( ( G e. USGraph /\ N e. V ) -> ( S e. USGraph <-> ( _I |` F ) : dom ( _I |` F ) -1-1-> { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )
27	18 26	mpbird	|- ( ( G e. USGraph /\ N e. V ) -> S e. USGraph )