Metamath Proof Explorer

Theorem vtxdginducedm1

Description: The degree of a vertex v in the induced subgraph S of a pseudograph G obtained by removing one vertex N plus the number of edges joining the vertex v and the vertex N is the degree of the vertex v in the pseudograph G . (Contributed by AV, 17-Dec-2021)

Ref Expression
Hypotheses vtxdginducedm1.v 
|- V = ( Vtx ` G )
vtxdginducedm1.e 
|- E = ( iEdg ` G )
vtxdginducedm1.k 
|- K = ( V \ { N } )
vtxdginducedm1.i 
|- I = { i e. dom E | N e/ ( E ` i ) }
vtxdginducedm1.p 
|- P = ( E |` I )
vtxdginducedm1.s 
|- S = <. K , P >.
vtxdginducedm1.j 
|- J = { i e. dom E | N e. ( E ` i ) }
Assertion vtxdginducedm1 
|- A. v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) +e ( # ` { l e. J | v e. ( E ` l ) } ) )

Proof

Step Hyp Ref Expression
1 vtxdginducedm1.v 
 |-  V = ( Vtx ` G )
2 vtxdginducedm1.e 
 |-  E = ( iEdg ` G )
3 vtxdginducedm1.k 
 |-  K = ( V \ { N } )
4 vtxdginducedm1.i 
 |-  I = { i e. dom E | N e/ ( E ` i ) }
5 vtxdginducedm1.p 
 |-  P = ( E |` I )
6 vtxdginducedm1.s 
 |-  S = <. K , P >.
7 vtxdginducedm1.j 
 |-  J = { i e. dom E | N e. ( E ` i ) }
8 7 4 elnelun 
 |-  ( J u. I ) = dom E
9 8 eqcomi 
 |-  dom E = ( J u. I )
10 9 rabeqi 
 |-  { k e. dom E | v e. ( E ` k ) } = { k e. ( J u. I ) | v e. ( E ` k ) }
11 rabun2 
 |-  { k e. ( J u. I ) | v e. ( E ` k ) } = ( { k e. J | v e. ( E ` k ) } u. { k e. I | v e. ( E ` k ) } )
12 10 11 eqtri 
 |-  { k e. dom E | v e. ( E ` k ) } = ( { k e. J | v e. ( E ` k ) } u. { k e. I | v e. ( E ` k ) } )
13 12 fveq2i 
 |-  ( # ` { k e. dom E | v e. ( E ` k ) } ) = ( # ` ( { k e. J | v e. ( E ` k ) } u. { k e. I | v e. ( E ` k ) } ) )
14 2 fvexi 
 |-  E e. _V
15 14 dmex 
 |-  dom E e. _V
16 7 15 rab2ex 
 |-  { k e. J | v e. ( E ` k ) } e. _V
17 4 15 rab2ex 
 |-  { k e. I | v e. ( E ` k ) } e. _V
18 ssrab2 
 |-  { k e. J | v e. ( E ` k ) } C_ J
19 ssrab2 
 |-  { k e. I | v e. ( E ` k ) } C_ I
20 ss2in 
 |-  ( ( { k e. J | v e. ( E ` k ) } C_ J /\ { k e. I | v e. ( E ` k ) } C_ I ) -> ( { k e. J | v e. ( E ` k ) } i^i { k e. I | v e. ( E ` k ) } ) C_ ( J i^i I ) )
21 18 19 20 mp2an 
 |-  ( { k e. J | v e. ( E ` k ) } i^i { k e. I | v e. ( E ` k ) } ) C_ ( J i^i I )
22 7 4 elneldisj 
 |-  ( J i^i I ) = (/)
23 22 sseq2i 
 |-  ( ( { k e. J | v e. ( E ` k ) } i^i { k e. I | v e. ( E ` k ) } ) C_ ( J i^i I ) <-> ( { k e. J | v e. ( E ` k ) } i^i { k e. I | v e. ( E ` k ) } ) C_ (/) )
24 ss0 
 |-  ( ( { k e. J | v e. ( E ` k ) } i^i { k e. I | v e. ( E ` k ) } ) C_ (/) -> ( { k e. J | v e. ( E ` k ) } i^i { k e. I | v e. ( E ` k ) } ) = (/) )
25 23 24 sylbi 
 |-  ( ( { k e. J | v e. ( E ` k ) } i^i { k e. I | v e. ( E ` k ) } ) C_ ( J i^i I ) -> ( { k e. J | v e. ( E ` k ) } i^i { k e. I | v e. ( E ` k ) } ) = (/) )
26 21 25 ax-mp 
 |-  ( { k e. J | v e. ( E ` k ) } i^i { k e. I | v e. ( E ` k ) } ) = (/)
27 hashunx 
 |-  ( ( { k e. J | v e. ( E ` k ) } e. _V /\ { k e. I | v e. ( E ` k ) } e. _V /\ ( { k e. J | v e. ( E ` k ) } i^i { k e. I | v e. ( E ` k ) } ) = (/) ) -> ( # ` ( { k e. J | v e. ( E ` k ) } u. { k e. I | v e. ( E ` k ) } ) ) = ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. I | v e. ( E ` k ) } ) ) )
28 16 17 26 27 mp3an 
 |-  ( # ` ( { k e. J | v e. ( E ` k ) } u. { k e. I | v e. ( E ` k ) } ) ) = ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. I | v e. ( E ` k ) } ) )
29 13 28 eqtri 
 |-  ( # ` { k e. dom E | v e. ( E ` k ) } ) = ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. I | v e. ( E ` k ) } ) )
30 9 rabeqi 
 |-  { k e. dom E | ( E ` k ) = { v } } = { k e. ( J u. I ) | ( E ` k ) = { v } }
31 rabun2 
 |-  { k e. ( J u. I ) | ( E ` k ) = { v } } = ( { k e. J | ( E ` k ) = { v } } u. { k e. I | ( E ` k ) = { v } } )
32 30 31 eqtri 
 |-  { k e. dom E | ( E ` k ) = { v } } = ( { k e. J | ( E ` k ) = { v } } u. { k e. I | ( E ` k ) = { v } } )
33 32 fveq2i 
 |-  ( # ` { k e. dom E | ( E ` k ) = { v } } ) = ( # ` ( { k e. J | ( E ` k ) = { v } } u. { k e. I | ( E ` k ) = { v } } ) )
34 7 15 rab2ex 
 |-  { k e. J | ( E ` k ) = { v } } e. _V
35 4 15 rab2ex 
 |-  { k e. I | ( E ` k ) = { v } } e. _V
36 ssrab2 
 |-  { k e. J | ( E ` k ) = { v } } C_ J
37 ssrab2 
 |-  { k e. I | ( E ` k ) = { v } } C_ I
38 ss2in 
 |-  ( ( { k e. J | ( E ` k ) = { v } } C_ J /\ { k e. I | ( E ` k ) = { v } } C_ I ) -> ( { k e. J | ( E ` k ) = { v } } i^i { k e. I | ( E ` k ) = { v } } ) C_ ( J i^i I ) )
39 36 37 38 mp2an 
 |-  ( { k e. J | ( E ` k ) = { v } } i^i { k e. I | ( E ` k ) = { v } } ) C_ ( J i^i I )
40 22 sseq2i 
 |-  ( ( { k e. J | ( E ` k ) = { v } } i^i { k e. I | ( E ` k ) = { v } } ) C_ ( J i^i I ) <-> ( { k e. J | ( E ` k ) = { v } } i^i { k e. I | ( E ` k ) = { v } } ) C_ (/) )
41 ss0 
 |-  ( ( { k e. J | ( E ` k ) = { v } } i^i { k e. I | ( E ` k ) = { v } } ) C_ (/) -> ( { k e. J | ( E ` k ) = { v } } i^i { k e. I | ( E ` k ) = { v } } ) = (/) )
42 40 41 sylbi 
 |-  ( ( { k e. J | ( E ` k ) = { v } } i^i { k e. I | ( E ` k ) = { v } } ) C_ ( J i^i I ) -> ( { k e. J | ( E ` k ) = { v } } i^i { k e. I | ( E ` k ) = { v } } ) = (/) )
43 39 42 ax-mp 
 |-  ( { k e. J | ( E ` k ) = { v } } i^i { k e. I | ( E ` k ) = { v } } ) = (/)
44 hashunx 
 |-  ( ( { k e. J | ( E ` k ) = { v } } e. _V /\ { k e. I | ( E ` k ) = { v } } e. _V /\ ( { k e. J | ( E ` k ) = { v } } i^i { k e. I | ( E ` k ) = { v } } ) = (/) ) -> ( # ` ( { k e. J | ( E ` k ) = { v } } u. { k e. I | ( E ` k ) = { v } } ) ) = ( ( # ` { k e. J | ( E ` k ) = { v } } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) )
45 34 35 43 44 mp3an 
 |-  ( # ` ( { k e. J | ( E ` k ) = { v } } u. { k e. I | ( E ` k ) = { v } } ) ) = ( ( # ` { k e. J | ( E ` k ) = { v } } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) )
46 33 45 eqtri 
 |-  ( # ` { k e. dom E | ( E ` k ) = { v } } ) = ( ( # ` { k e. J | ( E ` k ) = { v } } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) )
47 29 46 oveq12i 
 |-  ( ( # ` { k e. dom E | v e. ( E ` k ) } ) +e ( # ` { k e. dom E | ( E ` k ) = { v } } ) ) = ( ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. I | v e. ( E ` k ) } ) ) +e ( ( # ` { k e. J | ( E ` k ) = { v } } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) )
48 hashxnn0 
 |-  ( { k e. J | v e. ( E ` k ) } e. _V -> ( # ` { k e. J | v e. ( E ` k ) } ) e. NN0* )
49 16 48 ax-mp 
 |-  ( # ` { k e. J | v e. ( E ` k ) } ) e. NN0*
50 49 a1i 
 |-  ( v e. ( V \ { N } ) -> ( # ` { k e. J | v e. ( E ` k ) } ) e. NN0* )
51 hashxnn0 
 |-  ( { k e. I | v e. ( E ` k ) } e. _V -> ( # ` { k e. I | v e. ( E ` k ) } ) e. NN0* )
52 17 51 ax-mp 
 |-  ( # ` { k e. I | v e. ( E ` k ) } ) e. NN0*
53 52 a1i 
 |-  ( v e. ( V \ { N } ) -> ( # ` { k e. I | v e. ( E ` k ) } ) e. NN0* )
54 hashxnn0 
 |-  ( { k e. J | ( E ` k ) = { v } } e. _V -> ( # ` { k e. J | ( E ` k ) = { v } } ) e. NN0* )
55 34 54 ax-mp 
 |-  ( # ` { k e. J | ( E ` k ) = { v } } ) e. NN0*
56 55 a1i 
 |-  ( v e. ( V \ { N } ) -> ( # ` { k e. J | ( E ` k ) = { v } } ) e. NN0* )
57 hashxnn0 
 |-  ( { k e. I | ( E ` k ) = { v } } e. _V -> ( # ` { k e. I | ( E ` k ) = { v } } ) e. NN0* )
58 35 57 ax-mp 
 |-  ( # ` { k e. I | ( E ` k ) = { v } } ) e. NN0*
59 58 a1i 
 |-  ( v e. ( V \ { N } ) -> ( # ` { k e. I | ( E ` k ) = { v } } ) e. NN0* )
60 50 53 56 59 xnn0add4d 
 |-  ( v e. ( V \ { N } ) -> ( ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. I | v e. ( E ` k ) } ) ) +e ( ( # ` { k e. J | ( E ` k ) = { v } } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) ) = ( ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) +e ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) ) )
61 xnn0xaddcl 
 |-  ( ( ( # ` { k e. J | v e. ( E ` k ) } ) e. NN0* /\ ( # ` { k e. J | ( E ` k ) = { v } } ) e. NN0* ) -> ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) e. NN0* )
62 49 55 61 mp2an 
 |-  ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) e. NN0*
63 xnn0xr 
 |-  ( ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) e. NN0* -> ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) e. RR* )
64 62 63 ax-mp 
 |-  ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) e. RR*
65 xnn0xaddcl 
 |-  ( ( ( # ` { k e. I | v e. ( E ` k ) } ) e. NN0* /\ ( # ` { k e. I | ( E ` k ) = { v } } ) e. NN0* ) -> ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) e. NN0* )
66 52 58 65 mp2an 
 |-  ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) e. NN0*
67 xnn0xr 
 |-  ( ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) e. NN0* -> ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) e. RR* )
68 66 67 ax-mp 
 |-  ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) e. RR*
69 xaddcom 
 |-  ( ( ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) e. RR* /\ ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) e. RR* ) -> ( ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) +e ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) ) = ( ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) +e ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) ) )
70 64 68 69 mp2an 
 |-  ( ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) +e ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) ) = ( ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) +e ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) )
71 1 2 3 4 5 6 7 vtxdginducedm1lem4 
 |-  ( v e. ( V \ { N } ) -> ( # ` { k e. J | ( E ` k ) = { v } } ) = 0 )
72 71 oveq2d 
 |-  ( v e. ( V \ { N } ) -> ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) = ( ( # ` { k e. J | v e. ( E ` k ) } ) +e 0 ) )
73 xnn0xr 
 |-  ( ( # ` { k e. J | v e. ( E ` k ) } ) e. NN0* -> ( # ` { k e. J | v e. ( E ` k ) } ) e. RR* )
74 49 73 ax-mp 
 |-  ( # ` { k e. J | v e. ( E ` k ) } ) e. RR*
75 xaddid1 
 |-  ( ( # ` { k e. J | v e. ( E ` k ) } ) e. RR* -> ( ( # ` { k e. J | v e. ( E ` k ) } ) +e 0 ) = ( # ` { k e. J | v e. ( E ` k ) } ) )
76 74 75 ax-mp 
 |-  ( ( # ` { k e. J | v e. ( E ` k ) } ) +e 0 ) = ( # ` { k e. J | v e. ( E ` k ) } )
77 72 76 syl6eq 
 |-  ( v e. ( V \ { N } ) -> ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) = ( # ` { k e. J | v e. ( E ` k ) } ) )
78 fveq2 
 |-  ( k = l -> ( E ` k ) = ( E ` l ) )
79 78 eleq2d 
 |-  ( k = l -> ( v e. ( E ` k ) <-> v e. ( E ` l ) ) )
80 79 cbvrabv 
 |-  { k e. J | v e. ( E ` k ) } = { l e. J | v e. ( E ` l ) }
81 80 fveq2i 
 |-  ( # ` { k e. J | v e. ( E ` k ) } ) = ( # ` { l e. J | v e. ( E ` l ) } )
82 77 81 syl6eq 
 |-  ( v e. ( V \ { N } ) -> ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) = ( # ` { l e. J | v e. ( E ` l ) } ) )
83 82 oveq2d 
 |-  ( v e. ( V \ { N } ) -> ( ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) +e ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) ) = ( ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) )
84 70 83 syl5eq 
 |-  ( v e. ( V \ { N } ) -> ( ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. J | ( E ` k ) = { v } } ) ) +e ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) ) = ( ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) )
85 60 84 eqtrd 
 |-  ( v e. ( V \ { N } ) -> ( ( ( # ` { k e. J | v e. ( E ` k ) } ) +e ( # ` { k e. I | v e. ( E ` k ) } ) ) +e ( ( # ` { k e. J | ( E ` k ) = { v } } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) ) = ( ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) )
86 47 85 syl5eq 
 |-  ( v e. ( V \ { N } ) -> ( ( # ` { k e. dom E | v e. ( E ` k ) } ) +e ( # ` { k e. dom E | ( E ` k ) = { v } } ) ) = ( ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) )
87 1 2 3 4 5 6 vtxdginducedm1lem2 
 |-  dom ( iEdg ` S ) = I
88 87 rabeqi 
 |-  { k e. dom ( iEdg ` S ) | v e. ( ( iEdg ` S ) ` k ) } = { k e. I | v e. ( ( iEdg ` S ) ` k ) }
89 1 2 3 4 5 6 vtxdginducedm1lem3 
 |-  ( k e. I -> ( ( iEdg ` S ) ` k ) = ( E ` k ) )
90 89 eleq2d 
 |-  ( k e. I -> ( v e. ( ( iEdg ` S ) ` k ) <-> v e. ( E ` k ) ) )
91 90 rabbiia 
 |-  { k e. I | v e. ( ( iEdg ` S ) ` k ) } = { k e. I | v e. ( E ` k ) }
92 88 91 eqtri 
 |-  { k e. dom ( iEdg ` S ) | v e. ( ( iEdg ` S ) ` k ) } = { k e. I | v e. ( E ` k ) }
93 92 fveq2i 
 |-  ( # ` { k e. dom ( iEdg ` S ) | v e. ( ( iEdg ` S ) ` k ) } ) = ( # ` { k e. I | v e. ( E ` k ) } )
94 87 rabeqi 
 |-  { k e. dom ( iEdg ` S ) | ( ( iEdg ` S ) ` k ) = { v } } = { k e. I | ( ( iEdg ` S ) ` k ) = { v } }
95 89 eqeq1d 
 |-  ( k e. I -> ( ( ( iEdg ` S ) ` k ) = { v } <-> ( E ` k ) = { v } ) )
96 95 rabbiia 
 |-  { k e. I | ( ( iEdg ` S ) ` k ) = { v } } = { k e. I | ( E ` k ) = { v } }
97 94 96 eqtri 
 |-  { k e. dom ( iEdg ` S ) | ( ( iEdg ` S ) ` k ) = { v } } = { k e. I | ( E ` k ) = { v } }
98 97 fveq2i 
 |-  ( # ` { k e. dom ( iEdg ` S ) | ( ( iEdg ` S ) ` k ) = { v } } ) = ( # ` { k e. I | ( E ` k ) = { v } } )
99 93 98 oveq12i 
 |-  ( ( # ` { k e. dom ( iEdg ` S ) | v e. ( ( iEdg ` S ) ` k ) } ) +e ( # ` { k e. dom ( iEdg ` S ) | ( ( iEdg ` S ) ` k ) = { v } } ) ) = ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) )
100 99 eqcomi 
 |-  ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) = ( ( # ` { k e. dom ( iEdg ` S ) | v e. ( ( iEdg ` S ) ` k ) } ) +e ( # ` { k e. dom ( iEdg ` S ) | ( ( iEdg ` S ) ` k ) = { v } } ) )
101 100 oveq1i 
 |-  ( ( ( # ` { k e. I | v e. ( E ` k ) } ) +e ( # ` { k e. I | ( E ` k ) = { v } } ) ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) = ( ( ( # ` { k e. dom ( iEdg ` S ) | v e. ( ( iEdg ` S ) ` k ) } ) +e ( # ` { k e. dom ( iEdg ` S ) | ( ( iEdg ` S ) ` k ) = { v } } ) ) +e ( # ` { l e. J | v e. ( E ` l ) } ) )
102 86 101 syl6eq 
 |-  ( v e. ( V \ { N } ) -> ( ( # ` { k e. dom E | v e. ( E ` k ) } ) +e ( # ` { k e. dom E | ( E ` k ) = { v } } ) ) = ( ( ( # ` { k e. dom ( iEdg ` S ) | v e. ( ( iEdg ` S ) ` k ) } ) +e ( # ` { k e. dom ( iEdg ` S ) | ( ( iEdg ` S ) ` k ) = { v } } ) ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) )
103 eldifi 
 |-  ( v e. ( V \ { N } ) -> v e. V )
104 eqid 
 |-  dom E = dom E
105 1 2 104 vtxdgval 
 |-  ( v e. V -> ( ( VtxDeg ` G ) ` v ) = ( ( # ` { k e. dom E | v e. ( E ` k ) } ) +e ( # ` { k e. dom E | ( E ` k ) = { v } } ) ) )
106 103 105 syl 
 |-  ( v e. ( V \ { N } ) -> ( ( VtxDeg ` G ) ` v ) = ( ( # ` { k e. dom E | v e. ( E ` k ) } ) +e ( # ` { k e. dom E | ( E ` k ) = { v } } ) ) )
107 6 fveq2i 
 |-  ( Vtx ` S ) = ( Vtx ` <. K , P >. )
108 1 fvexi 
 |-  V e. _V
109 difexg 
 |-  ( V e. _V -> ( V \ { N } ) e. _V )
110 3 109 eqeltrid 
 |-  ( V e. _V -> K e. _V )
111 108 110 ax-mp 
 |-  K e. _V
112 resexg 
 |-  ( E e. _V -> ( E |` I ) e. _V )
113 5 112 eqeltrid 
 |-  ( E e. _V -> P e. _V )
114 14 113 ax-mp 
 |-  P e. _V
115 111 114 opvtxfvi 
 |-  ( Vtx ` <. K , P >. ) = K
116 107 115 eqtri 
 |-  ( Vtx ` S ) = K
117 116 eleq2i 
 |-  ( v e. ( Vtx ` S ) <-> v e. K )
118 3 eleq2i 
 |-  ( v e. K <-> v e. ( V \ { N } ) )
119 117 118 sylbbr 
 |-  ( v e. ( V \ { N } ) -> v e. ( Vtx ` S ) )
120 eqid 
 |-  ( Vtx ` S ) = ( Vtx ` S )
121 eqid 
 |-  ( iEdg ` S ) = ( iEdg ` S )
122 eqid 
 |-  dom ( iEdg ` S ) = dom ( iEdg ` S )
123 120 121 122 vtxdgval 
 |-  ( v e. ( Vtx ` S ) -> ( ( VtxDeg ` S ) ` v ) = ( ( # ` { k e. dom ( iEdg ` S ) | v e. ( ( iEdg ` S ) ` k ) } ) +e ( # ` { k e. dom ( iEdg ` S ) | ( ( iEdg ` S ) ` k ) = { v } } ) ) )
124 119 123 syl 
 |-  ( v e. ( V \ { N } ) -> ( ( VtxDeg ` S ) ` v ) = ( ( # ` { k e. dom ( iEdg ` S ) | v e. ( ( iEdg ` S ) ` k ) } ) +e ( # ` { k e. dom ( iEdg ` S ) | ( ( iEdg ` S ) ` k ) = { v } } ) ) )
125 124 oveq1d 
 |-  ( v e. ( V \ { N } ) -> ( ( ( VtxDeg ` S ) ` v ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) = ( ( ( # ` { k e. dom ( iEdg ` S ) | v e. ( ( iEdg ` S ) ` k ) } ) +e ( # ` { k e. dom ( iEdg ` S ) | ( ( iEdg ` S ) ` k ) = { v } } ) ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) )
126 102 106 125 3eqtr4d 
 |-  ( v e. ( V \ { N } ) -> ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) )
127 126 rgen 
 |-  A. v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) +e ( # ` { l e. J | v e. ( E ` l ) } ) )