Metamath Proof Explorer

Theorem p1evtxdp1

Description: If an edge E (not being a loop) which contains vertex U is added to a graph G (yielding a graph F ), the degree of U is increased by 1. (Contributed by AV, 3-Mar-2021)

Ref Expression
Hypotheses p1evtxdeq.v 
|- V = ( Vtx ` G )
p1evtxdeq.i 
|- I = ( iEdg ` G )
p1evtxdeq.f 
|- ( ph -> Fun I )
p1evtxdeq.fv 
|- ( ph -> ( Vtx ` F ) = V )
p1evtxdeq.fi 
|- ( ph -> ( iEdg ` F ) = ( I u. { <. K , E >. } ) )
p1evtxdeq.k 
|- ( ph -> K e. X )
p1evtxdeq.d 
|- ( ph -> K e/ dom I )
p1evtxdeq.u 
|- ( ph -> U e. V )
p1evtxdp1.e 
|- ( ph -> E e. ~P V )
p1evtxdp1.n 
|- ( ph -> U e. E )
p1evtxdp1.l 
|- ( ph -> 2 <_ ( # ` E ) )
Assertion p1evtxdp1 
|- ( ph -> ( ( VtxDeg ` F ) ` U ) = ( ( ( VtxDeg ` G ) ` U ) +e 1 ) )

Proof

Step Hyp Ref Expression
1 p1evtxdeq.v 
 |-  V = ( Vtx ` G )
2 p1evtxdeq.i 
 |-  I = ( iEdg ` G )
3 p1evtxdeq.f 
 |-  ( ph -> Fun I )
4 p1evtxdeq.fv 
 |-  ( ph -> ( Vtx ` F ) = V )
5 p1evtxdeq.fi 
 |-  ( ph -> ( iEdg ` F ) = ( I u. { <. K , E >. } ) )
6 p1evtxdeq.k 
 |-  ( ph -> K e. X )
7 p1evtxdeq.d 
 |-  ( ph -> K e/ dom I )
8 p1evtxdeq.u 
 |-  ( ph -> U e. V )
9 p1evtxdp1.e 
 |-  ( ph -> E e. ~P V )
10 p1evtxdp1.n 
 |-  ( ph -> U e. E )
11 p1evtxdp1.l 
 |-  ( ph -> 2 <_ ( # ` E ) )
12 1 2 3 4 5 6 7 8 9 p1evtxdeqlem 
 |-  ( ph -> ( ( VtxDeg ` F ) ` U ) = ( ( ( VtxDeg ` G ) ` U ) +e ( ( VtxDeg ` <. V , { <. K , E >. } >. ) ` U ) ) )
13 1 fvexi 
 |-  V e. _V
14 snex 
 |-  { <. K , E >. } e. _V
15 13 14 pm3.2i 
 |-  ( V e. _V /\ { <. K , E >. } e. _V )
16 opiedgfv 
 |-  ( ( V e. _V /\ { <. K , E >. } e. _V ) -> ( iEdg ` <. V , { <. K , E >. } >. ) = { <. K , E >. } )
17 15 16 mp1i 
 |-  ( ph -> ( iEdg ` <. V , { <. K , E >. } >. ) = { <. K , E >. } )
18 opvtxfv 
 |-  ( ( V e. _V /\ { <. K , E >. } e. _V ) -> ( Vtx ` <. V , { <. K , E >. } >. ) = V )
19 15 18 mp1i 
 |-  ( ph -> ( Vtx ` <. V , { <. K , E >. } >. ) = V )
20 17 19 6 8 9 10 11 1hevtxdg1 
 |-  ( ph -> ( ( VtxDeg ` <. V , { <. K , E >. } >. ) ` U ) = 1 )
21 20 oveq2d 
 |-  ( ph -> ( ( ( VtxDeg ` G ) ` U ) +e ( ( VtxDeg ` <. V , { <. K , E >. } >. ) ` U ) ) = ( ( ( VtxDeg ` G ) ` U ) +e 1 ) )
22 12 21 eqtrd 
 |-  ( ph -> ( ( VtxDeg ` F ) ` U ) = ( ( ( VtxDeg ` G ) ` U ) +e 1 ) )