Metamath Proof Explorer

Theorem vtxdun

Description: The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 21-Dec-2017) (Revised by AV, 19-Feb-2021)

Ref Expression
Hypotheses vtxdun.i 
|- I = ( iEdg ` G )
vtxdun.j 
|- J = ( iEdg ` H )
vtxdun.vg 
|- V = ( Vtx ` G )
vtxdun.vh 
|- ( ph -> ( Vtx ` H ) = V )
vtxdun.vu 
|- ( ph -> ( Vtx ` U ) = V )
vtxdun.d 
|- ( ph -> ( dom I i^i dom J ) = (/) )
vtxdun.fi 
|- ( ph -> Fun I )
vtxdun.fj 
|- ( ph -> Fun J )
vtxdun.n 
|- ( ph -> N e. V )
vtxdun.u 
|- ( ph -> ( iEdg ` U ) = ( I u. J ) )
Assertion vtxdun 
|- ( ph -> ( ( VtxDeg ` U ) ` N ) = ( ( ( VtxDeg ` G ) ` N ) +e ( ( VtxDeg ` H ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 vtxdun.i 
 |-  I = ( iEdg ` G )
2 vtxdun.j 
 |-  J = ( iEdg ` H )
3 vtxdun.vg 
 |-  V = ( Vtx ` G )
4 vtxdun.vh 
 |-  ( ph -> ( Vtx ` H ) = V )
5 vtxdun.vu 
 |-  ( ph -> ( Vtx ` U ) = V )
6 vtxdun.d 
 |-  ( ph -> ( dom I i^i dom J ) = (/) )
7 vtxdun.fi 
 |-  ( ph -> Fun I )
8 vtxdun.fj 
 |-  ( ph -> Fun J )
9 vtxdun.n 
 |-  ( ph -> N e. V )
10 vtxdun.u 
 |-  ( ph -> ( iEdg ` U ) = ( I u. J ) )
11 df-rab 
 |-  { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } = { x | ( x e. dom ( iEdg ` U ) /\ N e. ( ( iEdg ` U ) ` x ) ) }
12 10 dmeqd 
 |-  ( ph -> dom ( iEdg ` U ) = dom ( I u. J ) )
13 dmun 
 |-  dom ( I u. J ) = ( dom I u. dom J )
14 12 13 eqtrdi 
 |-  ( ph -> dom ( iEdg ` U ) = ( dom I u. dom J ) )
15 14 eleq2d 
 |-  ( ph -> ( x e. dom ( iEdg ` U ) <-> x e. ( dom I u. dom J ) ) )
16 elun 
 |-  ( x e. ( dom I u. dom J ) <-> ( x e. dom I \/ x e. dom J ) )
17 15 16 bitrdi 
 |-  ( ph -> ( x e. dom ( iEdg ` U ) <-> ( x e. dom I \/ x e. dom J ) ) )
18 17 anbi1d 
 |-  ( ph -> ( ( x e. dom ( iEdg ` U ) /\ N e. ( ( iEdg ` U ) ` x ) ) <-> ( ( x e. dom I \/ x e. dom J ) /\ N e. ( ( iEdg ` U ) ` x ) ) ) )
19 andir 
 |-  ( ( ( x e. dom I \/ x e. dom J ) /\ N e. ( ( iEdg ` U ) ` x ) ) <-> ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) )
20 18 19 bitrdi 
 |-  ( ph -> ( ( x e. dom ( iEdg ` U ) /\ N e. ( ( iEdg ` U ) ` x ) ) <-> ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) ) )
21 20 abbidv 
 |-  ( ph -> { x | ( x e. dom ( iEdg ` U ) /\ N e. ( ( iEdg ` U ) ` x ) ) } = { x | ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) } )
22 11 21 eqtrid 
 |-  ( ph -> { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } = { x | ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) } )
23 unab 
 |-  ( { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) } u. { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) } ) = { x | ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) }
24 23 eqcomi 
 |-  { x | ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) } = ( { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) } u. { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) } )
25 24 a1i 
 |-  ( ph -> { x | ( ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) \/ ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) ) } = ( { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) } u. { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) } ) )
26 df-rab 
 |-  { x e. dom I | N e. ( ( iEdg ` U ) ` x ) } = { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) }
27 10 fveq1d 
 |-  ( ph -> ( ( iEdg ` U ) ` x ) = ( ( I u. J ) ` x ) )
28 27 adantr 
 |-  ( ( ph /\ x e. dom I ) -> ( ( iEdg ` U ) ` x ) = ( ( I u. J ) ` x ) )
29 7 funfnd 
 |-  ( ph -> I Fn dom I )
30 29 adantr 
 |-  ( ( ph /\ x e. dom I ) -> I Fn dom I )
31 8 funfnd 
 |-  ( ph -> J Fn dom J )
32 31 adantr 
 |-  ( ( ph /\ x e. dom I ) -> J Fn dom J )
33 6 anim1i 
 |-  ( ( ph /\ x e. dom I ) -> ( ( dom I i^i dom J ) = (/) /\ x e. dom I ) )
34 fvun1 
 |-  ( ( I Fn dom I /\ J Fn dom J /\ ( ( dom I i^i dom J ) = (/) /\ x e. dom I ) ) -> ( ( I u. J ) ` x ) = ( I ` x ) )
35 30 32 33 34 syl3anc 
 |-  ( ( ph /\ x e. dom I ) -> ( ( I u. J ) ` x ) = ( I ` x ) )
36 28 35 eqtrd 
 |-  ( ( ph /\ x e. dom I ) -> ( ( iEdg ` U ) ` x ) = ( I ` x ) )
37 36 eleq2d 
 |-  ( ( ph /\ x e. dom I ) -> ( N e. ( ( iEdg ` U ) ` x ) <-> N e. ( I ` x ) ) )
38 37 rabbidva 
 |-  ( ph -> { x e. dom I | N e. ( ( iEdg ` U ) ` x ) } = { x e. dom I | N e. ( I ` x ) } )
39 26 38 eqtr3id 
 |-  ( ph -> { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) } = { x e. dom I | N e. ( I ` x ) } )
40 df-rab 
 |-  { x e. dom J | N e. ( ( iEdg ` U ) ` x ) } = { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) }
41 27 adantr 
 |-  ( ( ph /\ x e. dom J ) -> ( ( iEdg ` U ) ` x ) = ( ( I u. J ) ` x ) )
42 29 adantr 
 |-  ( ( ph /\ x e. dom J ) -> I Fn dom I )
43 31 adantr 
 |-  ( ( ph /\ x e. dom J ) -> J Fn dom J )
44 6 anim1i 
 |-  ( ( ph /\ x e. dom J ) -> ( ( dom I i^i dom J ) = (/) /\ x e. dom J ) )
45 fvun2 
 |-  ( ( I Fn dom I /\ J Fn dom J /\ ( ( dom I i^i dom J ) = (/) /\ x e. dom J ) ) -> ( ( I u. J ) ` x ) = ( J ` x ) )
46 42 43 44 45 syl3anc 
 |-  ( ( ph /\ x e. dom J ) -> ( ( I u. J ) ` x ) = ( J ` x ) )
47 41 46 eqtrd 
 |-  ( ( ph /\ x e. dom J ) -> ( ( iEdg ` U ) ` x ) = ( J ` x ) )
48 47 eleq2d 
 |-  ( ( ph /\ x e. dom J ) -> ( N e. ( ( iEdg ` U ) ` x ) <-> N e. ( J ` x ) ) )
49 48 rabbidva 
 |-  ( ph -> { x e. dom J | N e. ( ( iEdg ` U ) ` x ) } = { x e. dom J | N e. ( J ` x ) } )
50 40 49 eqtr3id 
 |-  ( ph -> { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) } = { x e. dom J | N e. ( J ` x ) } )
51 39 50 uneq12d 
 |-  ( ph -> ( { x | ( x e. dom I /\ N e. ( ( iEdg ` U ) ` x ) ) } u. { x | ( x e. dom J /\ N e. ( ( iEdg ` U ) ` x ) ) } ) = ( { x e. dom I | N e. ( I ` x ) } u. { x e. dom J | N e. ( J ` x ) } ) )
52 22 25 51 3eqtrd 
 |-  ( ph -> { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } = ( { x e. dom I | N e. ( I ` x ) } u. { x e. dom J | N e. ( J ` x ) } ) )
53 52 fveq2d 
 |-  ( ph -> ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) = ( # ` ( { x e. dom I | N e. ( I ` x ) } u. { x e. dom J | N e. ( J ` x ) } ) ) )
54 1 fvexi 
 |-  I e. _V
55 54 dmex 
 |-  dom I e. _V
56 55 rabex 
 |-  { x e. dom I | N e. ( I ` x ) } e. _V
57 56 a1i 
 |-  ( ph -> { x e. dom I | N e. ( I ` x ) } e. _V )
58 2 fvexi 
 |-  J e. _V
59 58 dmex 
 |-  dom J e. _V
60 59 rabex 
 |-  { x e. dom J | N e. ( J ` x ) } e. _V
61 60 a1i 
 |-  ( ph -> { x e. dom J | N e. ( J ` x ) } e. _V )
62 ssrab2 
 |-  { x e. dom I | N e. ( I ` x ) } C_ dom I
63 ssrab2 
 |-  { x e. dom J | N e. ( J ` x ) } C_ dom J
64 ss2in 
 |-  ( ( { x e. dom I | N e. ( I ` x ) } C_ dom I /\ { x e. dom J | N e. ( J ` x ) } C_ dom J ) -> ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) C_ ( dom I i^i dom J ) )
65 62 63 64 mp2an 
 |-  ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) C_ ( dom I i^i dom J )
66 65 6 sseqtrid 
 |-  ( ph -> ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) C_ (/) )
67 ss0 
 |-  ( ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) C_ (/) -> ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) = (/) )
68 66 67 syl 
 |-  ( ph -> ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) = (/) )
69 hashunx 
 |-  ( ( { x e. dom I | N e. ( I ` x ) } e. _V /\ { x e. dom J | N e. ( J ` x ) } e. _V /\ ( { x e. dom I | N e. ( I ` x ) } i^i { x e. dom J | N e. ( J ` x ) } ) = (/) ) -> ( # ` ( { x e. dom I | N e. ( I ` x ) } u. { x e. dom J | N e. ( J ` x ) } ) ) = ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom J | N e. ( J ` x ) } ) ) )
70 57 61 68 69 syl3anc 
 |-  ( ph -> ( # ` ( { x e. dom I | N e. ( I ` x ) } u. { x e. dom J | N e. ( J ` x ) } ) ) = ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom J | N e. ( J ` x ) } ) ) )
71 53 70 eqtrd 
 |-  ( ph -> ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) = ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom J | N e. ( J ` x ) } ) ) )
72 df-rab 
 |-  { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } = { x | ( x e. dom ( iEdg ` U ) /\ ( ( iEdg ` U ) ` x ) = { N } ) }
73 17 anbi1d 
 |-  ( ph -> ( ( x e. dom ( iEdg ` U ) /\ ( ( iEdg ` U ) ` x ) = { N } ) <-> ( ( x e. dom I \/ x e. dom J ) /\ ( ( iEdg ` U ) ` x ) = { N } ) ) )
74 andir 
 |-  ( ( ( x e. dom I \/ x e. dom J ) /\ ( ( iEdg ` U ) ` x ) = { N } ) <-> ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) )
75 73 74 bitrdi 
 |-  ( ph -> ( ( x e. dom ( iEdg ` U ) /\ ( ( iEdg ` U ) ` x ) = { N } ) <-> ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) ) )
76 75 abbidv 
 |-  ( ph -> { x | ( x e. dom ( iEdg ` U ) /\ ( ( iEdg ` U ) ` x ) = { N } ) } = { x | ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) } )
77 72 76 eqtrid 
 |-  ( ph -> { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } = { x | ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) } )
78 unab 
 |-  ( { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) } u. { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) } ) = { x | ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) }
79 78 eqcomi 
 |-  { x | ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) } = ( { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) } u. { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) } )
80 79 a1i 
 |-  ( ph -> { x | ( ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) \/ ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) ) } = ( { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) } u. { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) } ) )
81 df-rab 
 |-  { x e. dom I | ( ( iEdg ` U ) ` x ) = { N } } = { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) }
82 36 eqeq1d 
 |-  ( ( ph /\ x e. dom I ) -> ( ( ( iEdg ` U ) ` x ) = { N } <-> ( I ` x ) = { N } ) )
83 82 rabbidva 
 |-  ( ph -> { x e. dom I | ( ( iEdg ` U ) ` x ) = { N } } = { x e. dom I | ( I ` x ) = { N } } )
84 81 83 eqtr3id 
 |-  ( ph -> { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) } = { x e. dom I | ( I ` x ) = { N } } )
85 df-rab 
 |-  { x e. dom J | ( ( iEdg ` U ) ` x ) = { N } } = { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) }
86 47 eqeq1d 
 |-  ( ( ph /\ x e. dom J ) -> ( ( ( iEdg ` U ) ` x ) = { N } <-> ( J ` x ) = { N } ) )
87 86 rabbidva 
 |-  ( ph -> { x e. dom J | ( ( iEdg ` U ) ` x ) = { N } } = { x e. dom J | ( J ` x ) = { N } } )
88 85 87 eqtr3id 
 |-  ( ph -> { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) } = { x e. dom J | ( J ` x ) = { N } } )
89 84 88 uneq12d 
 |-  ( ph -> ( { x | ( x e. dom I /\ ( ( iEdg ` U ) ` x ) = { N } ) } u. { x | ( x e. dom J /\ ( ( iEdg ` U ) ` x ) = { N } ) } ) = ( { x e. dom I | ( I ` x ) = { N } } u. { x e. dom J | ( J ` x ) = { N } } ) )
90 77 80 89 3eqtrd 
 |-  ( ph -> { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } = ( { x e. dom I | ( I ` x ) = { N } } u. { x e. dom J | ( J ` x ) = { N } } ) )
91 90 fveq2d 
 |-  ( ph -> ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) = ( # ` ( { x e. dom I | ( I ` x ) = { N } } u. { x e. dom J | ( J ` x ) = { N } } ) ) )
92 55 rabex 
 |-  { x e. dom I | ( I ` x ) = { N } } e. _V
93 92 a1i 
 |-  ( ph -> { x e. dom I | ( I ` x ) = { N } } e. _V )
94 59 rabex 
 |-  { x e. dom J | ( J ` x ) = { N } } e. _V
95 94 a1i 
 |-  ( ph -> { x e. dom J | ( J ` x ) = { N } } e. _V )
96 ssrab2 
 |-  { x e. dom I | ( I ` x ) = { N } } C_ dom I
97 ssrab2 
 |-  { x e. dom J | ( J ` x ) = { N } } C_ dom J
98 ss2in 
 |-  ( ( { x e. dom I | ( I ` x ) = { N } } C_ dom I /\ { x e. dom J | ( J ` x ) = { N } } C_ dom J ) -> ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) C_ ( dom I i^i dom J ) )
99 96 97 98 mp2an 
 |-  ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) C_ ( dom I i^i dom J )
100 99 6 sseqtrid 
 |-  ( ph -> ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) C_ (/) )
101 ss0 
 |-  ( ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) C_ (/) -> ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) = (/) )
102 100 101 syl 
 |-  ( ph -> ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) = (/) )
103 hashunx 
 |-  ( ( { x e. dom I | ( I ` x ) = { N } } e. _V /\ { x e. dom J | ( J ` x ) = { N } } e. _V /\ ( { x e. dom I | ( I ` x ) = { N } } i^i { x e. dom J | ( J ` x ) = { N } } ) = (/) ) -> ( # ` ( { x e. dom I | ( I ` x ) = { N } } u. { x e. dom J | ( J ` x ) = { N } } ) ) = ( ( # ` { x e. dom I | ( I ` x ) = { N } } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) )
104 93 95 102 103 syl3anc 
 |-  ( ph -> ( # ` ( { x e. dom I | ( I ` x ) = { N } } u. { x e. dom J | ( J ` x ) = { N } } ) ) = ( ( # ` { x e. dom I | ( I ` x ) = { N } } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) )
105 91 104 eqtrd 
 |-  ( ph -> ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) = ( ( # ` { x e. dom I | ( I ` x ) = { N } } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) )
106 71 105 oveq12d 
 |-  ( ph -> ( ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) ) = ( ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom J | N e. ( J ` x ) } ) ) +e ( ( # ` { x e. dom I | ( I ` x ) = { N } } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) )
107 hashxnn0 
 |-  ( { x e. dom I | N e. ( I ` x ) } e. _V -> ( # ` { x e. dom I | N e. ( I ` x ) } ) e. NN0* )
108 57 107 syl 
 |-  ( ph -> ( # ` { x e. dom I | N e. ( I ` x ) } ) e. NN0* )
109 hashxnn0 
 |-  ( { x e. dom J | N e. ( J ` x ) } e. _V -> ( # ` { x e. dom J | N e. ( J ` x ) } ) e. NN0* )
110 61 109 syl 
 |-  ( ph -> ( # ` { x e. dom J | N e. ( J ` x ) } ) e. NN0* )
111 hashxnn0 
 |-  ( { x e. dom I | ( I ` x ) = { N } } e. _V -> ( # ` { x e. dom I | ( I ` x ) = { N } } ) e. NN0* )
112 93 111 syl 
 |-  ( ph -> ( # ` { x e. dom I | ( I ` x ) = { N } } ) e. NN0* )
113 hashxnn0 
 |-  ( { x e. dom J | ( J ` x ) = { N } } e. _V -> ( # ` { x e. dom J | ( J ` x ) = { N } } ) e. NN0* )
114 95 113 syl 
 |-  ( ph -> ( # ` { x e. dom J | ( J ` x ) = { N } } ) e. NN0* )
115 108 110 112 114 xnn0add4d 
 |-  ( ph -> ( ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom J | N e. ( J ` x ) } ) ) +e ( ( # ` { x e. dom I | ( I ` x ) = { N } } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) = ( ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom I | ( I ` x ) = { N } } ) ) +e ( ( # ` { x e. dom J | N e. ( J ` x ) } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) )
116 106 115 eqtrd 
 |-  ( ph -> ( ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) ) = ( ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom I | ( I ` x ) = { N } } ) ) +e ( ( # ` { x e. dom J | N e. ( J ` x ) } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) )
117 9 5 eleqtrrd 
 |-  ( ph -> N e. ( Vtx ` U ) )
118 eqid 
 |-  ( Vtx ` U ) = ( Vtx ` U )
119 eqid 
 |-  ( iEdg ` U ) = ( iEdg ` U )
120 eqid 
 |-  dom ( iEdg ` U ) = dom ( iEdg ` U )
121 118 119 120 vtxdgval 
 |-  ( N e. ( Vtx ` U ) -> ( ( VtxDeg ` U ) ` N ) = ( ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) ) )
122 117 121 syl 
 |-  ( ph -> ( ( VtxDeg ` U ) ` N ) = ( ( # ` { x e. dom ( iEdg ` U ) | N e. ( ( iEdg ` U ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` U ) | ( ( iEdg ` U ) ` x ) = { N } } ) ) )
123 eqid 
 |-  dom I = dom I
124 3 1 123 vtxdgval 
 |-  ( N e. V -> ( ( VtxDeg ` G ) ` N ) = ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom I | ( I ` x ) = { N } } ) ) )
125 9 124 syl 
 |-  ( ph -> ( ( VtxDeg ` G ) ` N ) = ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom I | ( I ` x ) = { N } } ) ) )
126 9 4 eleqtrrd 
 |-  ( ph -> N e. ( Vtx ` H ) )
127 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
128 eqid 
 |-  dom J = dom J
129 127 2 128 vtxdgval 
 |-  ( N e. ( Vtx ` H ) -> ( ( VtxDeg ` H ) ` N ) = ( ( # ` { x e. dom J | N e. ( J ` x ) } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) )
130 126 129 syl 
 |-  ( ph -> ( ( VtxDeg ` H ) ` N ) = ( ( # ` { x e. dom J | N e. ( J ` x ) } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) )
131 125 130 oveq12d 
 |-  ( ph -> ( ( ( VtxDeg ` G ) ` N ) +e ( ( VtxDeg ` H ) ` N ) ) = ( ( ( # ` { x e. dom I | N e. ( I ` x ) } ) +e ( # ` { x e. dom I | ( I ` x ) = { N } } ) ) +e ( ( # ` { x e. dom J | N e. ( J ` x ) } ) +e ( # ` { x e. dom J | ( J ` x ) = { N } } ) ) ) )
132 116 122 131 3eqtr4d 
 |-  ( ph -> ( ( VtxDeg ` U ) ` N ) = ( ( ( VtxDeg ` G ) ` N ) +e ( ( VtxDeg ` H ) ` N ) ) )