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 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
vtxdun.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
vtxdun.vg ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdun.vh ⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
vtxdun.vu ⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
vtxdun.d ⊢ ( 𝜑 → ( dom 𝐼 ∩ dom 𝐽 ) = ∅ )
vtxdun.fi ⊢ ( 𝜑 → Fun 𝐼 )
vtxdun.fj ⊢ ( 𝜑 → Fun 𝐽 )
vtxdun.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
vtxdun.u ⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐼 ∪ 𝐽 ) )
Assertion vtxdun ( 𝜑 → ( ( VtxDeg ‘ 𝑈 ) ‘ 𝑁 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) +𝑒 ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑁 ) ) )

Proof

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