Metamath Proof Explorer

Theorem upgrres1

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

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. UPGraph /\ N e. V ) -> ( _I |` F ) : F --> F )
8 7 ffdmd 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( _I |` F ) : dom ( _I |` F ) --> F )
9 simpr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ e e. E ) -> e e. E )
10 9 adantr 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ e e. E ) /\ N e/ e ) -> e e. E )
11 2 eleq2i 
 |-  ( e e. E <-> e e. ( Edg ` G ) )
12 edgupgr 
 |-  ( ( G e. UPGraph /\ e e. ( Edg ` G ) ) -> ( e e. ~P ( Vtx ` G ) /\ e =/= (/) /\ ( # ` e ) <_ 2 ) )
13 elpwi 
 |-  ( e e. ~P ( Vtx ` G ) -> e C_ ( Vtx ` G ) )
14 13 1 sseqtrrdi 
 |-  ( e e. ~P ( Vtx ` G ) -> e C_ V )
15 14 3ad2ant1 
 |-  ( ( e e. ~P ( Vtx ` G ) /\ e =/= (/) /\ ( # ` e ) <_ 2 ) -> e C_ V )
16 12 15 syl 
 |-  ( ( G e. UPGraph /\ e e. ( Edg ` G ) ) -> e C_ V )
17 11 16 sylan2b 
 |-  ( ( G e. UPGraph /\ e e. E ) -> e C_ V )
18 17 ad4ant13 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ e e. E ) /\ N e/ e ) -> e C_ V )
19 simpr 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ e e. E ) /\ N e/ e ) -> N e/ e )
20 elpwdifsn 
 |-  ( ( e e. E /\ e C_ V /\ N e/ e ) -> e e. ~P ( V \ { N } ) )
21 10 18 19 20 syl3anc 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ e e. E ) /\ N e/ e ) -> e e. ~P ( V \ { N } ) )
22 simpl 
 |-  ( ( G e. UPGraph /\ N e. V ) -> G e. UPGraph )
23 11 biimpi 
 |-  ( e e. E -> e e. ( Edg ` G ) )
24 12 simp2d 
 |-  ( ( G e. UPGraph /\ e e. ( Edg ` G ) ) -> e =/= (/) )
25 22 23 24 syl2an 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ e e. E ) -> e =/= (/) )
26 25 adantr 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ e e. E ) /\ N e/ e ) -> e =/= (/) )
27 nelsn 
 |-  ( e =/= (/) -> -. e e. { (/) } )
28 26 27 syl 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ e e. E ) /\ N e/ e ) -> -. e e. { (/) } )
29 21 28 eldifd 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ e e. E ) /\ N e/ e ) -> e e. ( ~P ( V \ { N } ) \ { (/) } ) )
30 29 ex 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ e e. E ) -> ( N e/ e -> e e. ( ~P ( V \ { N } ) \ { (/) } ) ) )
31 30 ralrimiva 
 |-  ( ( G e. UPGraph /\ N e. V ) -> A. e e. E ( N e/ e -> e e. ( ~P ( V \ { N } ) \ { (/) } ) ) )
32 rabss 
 |-  ( { e e. E | N e/ e } C_ ( ~P ( V \ { N } ) \ { (/) } ) <-> A. e e. E ( N e/ e -> e e. ( ~P ( V \ { N } ) \ { (/) } ) ) )
33 31 32 sylibr 
 |-  ( ( G e. UPGraph /\ N e. V ) -> { e e. E | N e/ e } C_ ( ~P ( V \ { N } ) \ { (/) } ) )
34 3 33 eqsstrid 
 |-  ( ( G e. UPGraph /\ N e. V ) -> F C_ ( ~P ( V \ { N } ) \ { (/) } ) )
35 elrabi 
 |-  ( p e. { e e. E | N e/ e } -> p e. E )
36 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
37 2 36 eqtri 
 |-  E = ran ( iEdg ` G )
38 37 eleq2i 
 |-  ( p e. E <-> p e. ran ( iEdg ` G ) )
39 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
40 1 39 upgrf 
 |-  ( G e. UPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
41 40 frnd 
 |-  ( G e. UPGraph -> ran ( iEdg ` G ) C_ { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
42 41 sseld 
 |-  ( G e. UPGraph -> ( p e. ran ( iEdg ` G ) -> p e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
43 38 42 syl5bi 
 |-  ( G e. UPGraph -> ( p e. E -> p e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
44 fveq2 
 |-  ( x = p -> ( # ` x ) = ( # ` p ) )
45 44 breq1d 
 |-  ( x = p -> ( ( # ` x ) <_ 2 <-> ( # ` p ) <_ 2 ) )
46 45 elrab 
 |-  ( p e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } <-> ( p e. ( ~P V \ { (/) } ) /\ ( # ` p ) <_ 2 ) )
47 46 simprbi 
 |-  ( p e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> ( # ` p ) <_ 2 )
48 43 47 syl6 
 |-  ( G e. UPGraph -> ( p e. E -> ( # ` p ) <_ 2 ) )
49 48 adantr 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( p e. E -> ( # ` p ) <_ 2 ) )
50 35 49 syl5com 
 |-  ( p e. { e e. E | N e/ e } -> ( ( G e. UPGraph /\ N e. V ) -> ( # ` p ) <_ 2 ) )
51 50 3 eleq2s 
 |-  ( p e. F -> ( ( G e. UPGraph /\ N e. V ) -> ( # ` p ) <_ 2 ) )
52 51 impcom 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ p e. F ) -> ( # ` p ) <_ 2 )
53 34 52 ssrabdv 
 |-  ( ( G e. UPGraph /\ N e. V ) -> F C_ { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } )
54 8 53 fssd 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( _I |` F ) : dom ( _I |` F ) --> { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } )
55 opex 
 |-  <. ( V \ { N } ) , ( _I |` F ) >. e. _V
56 4 55 eqeltri 
 |-  S e. _V
57 1 2 3 4 upgrres1lem2 
 |-  ( Vtx ` S ) = ( V \ { N } )
58 57 eqcomi 
 |-  ( V \ { N } ) = ( Vtx ` S )
59 1 2 3 4 upgrres1lem3 
 |-  ( iEdg ` S ) = ( _I |` F )
60 59 eqcomi 
 |-  ( _I |` F ) = ( iEdg ` S )
61 58 60 isupgr 
 |-  ( S e. _V -> ( S e. UPGraph <-> ( _I |` F ) : dom ( _I |` F ) --> { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
62 56 61 mp1i 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( S e. UPGraph <-> ( _I |` F ) : dom ( _I |` F ) --> { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
63 54 62 mpbird 
 |-  ( ( G e. UPGraph /\ N e. V ) -> S e. UPGraph )