Metamath Proof Explorer

Theorem p1evtxdeqlem

Description: Lemma for p1evtxdeq and p1evtxdp1 . (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 )
p1evtxdeq.e 
|- ( ph -> E e. Y )
Assertion p1evtxdeqlem 
|- ( ph -> ( ( VtxDeg ` F ) ` U ) = ( ( ( VtxDeg ` G ) ` U ) +e ( ( VtxDeg ` <. V , { <. K , E >. } >. ) ` U ) ) )

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 p1evtxdeq.e 
 |-  ( ph -> E e. Y )
10 1 fvexi 
 |-  V e. _V
11 snex 
 |-  { <. K , E >. } e. _V
12 10 11 pm3.2i 
 |-  ( V e. _V /\ { <. K , E >. } e. _V )
13 opiedgfv 
 |-  ( ( V e. _V /\ { <. K , E >. } e. _V ) -> ( iEdg ` <. V , { <. K , E >. } >. ) = { <. K , E >. } )
14 13 eqcomd 
 |-  ( ( V e. _V /\ { <. K , E >. } e. _V ) -> { <. K , E >. } = ( iEdg ` <. V , { <. K , E >. } >. ) )
15 12 14 ax-mp 
 |-  { <. K , E >. } = ( iEdg ` <. V , { <. K , E >. } >. )
16 opvtxfv 
 |-  ( ( V e. _V /\ { <. K , E >. } e. _V ) -> ( Vtx ` <. V , { <. K , E >. } >. ) = V )
17 12 16 mp1i 
 |-  ( ph -> ( Vtx ` <. V , { <. K , E >. } >. ) = V )
18 dmsnopg 
 |-  ( E e. Y -> dom { <. K , E >. } = { K } )
19 9 18 syl 
 |-  ( ph -> dom { <. K , E >. } = { K } )
20 19 ineq2d 
 |-  ( ph -> ( dom I i^i dom { <. K , E >. } ) = ( dom I i^i { K } ) )
21 df-nel 
 |-  ( K e/ dom I <-> -. K e. dom I )
22 7 21 sylib 
 |-  ( ph -> -. K e. dom I )
23 disjsn 
 |-  ( ( dom I i^i { K } ) = (/) <-> -. K e. dom I )
24 22 23 sylibr 
 |-  ( ph -> ( dom I i^i { K } ) = (/) )
25 20 24 eqtrd 
 |-  ( ph -> ( dom I i^i dom { <. K , E >. } ) = (/) )
26 funsng 
 |-  ( ( K e. X /\ E e. Y ) -> Fun { <. K , E >. } )
27 6 9 26 syl2anc 
 |-  ( ph -> Fun { <. K , E >. } )
28 2 15 1 17 4 25 3 27 8 5 vtxdun 
 |-  ( ph -> ( ( VtxDeg ` F ) ` U ) = ( ( ( VtxDeg ` G ) ` U ) +e ( ( VtxDeg ` <. V , { <. K , E >. } >. ) ` U ) ) )