This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )