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	eqtrid	⊢ ( 𝜑 → { 𝑥 ∈ 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	eqtr3id	⊢ ( 𝜑 → { 𝑥 ∣ ( 𝑥 ∈ 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	eqtr3id	⊢ ( 𝜑 → { 𝑥 ∣ ( 𝑥 ∈ 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	eqtrid	⊢ ( 𝜑 → { 𝑥 ∈ 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	eqtr3id	⊢ ( 𝜑 → { 𝑥 ∣ ( 𝑥 ∈ dom 𝐼 ∧ ( ( iEdg ‘ 𝑈 ) ‘ 𝑥 ) = { 𝑁 } ) } = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑁 } } )
85		df-rab	⊢ { 𝑥 ∈ dom 𝐽 ∣ ( ( iEdg ‘ 𝑈 ) ‘ 𝑥 ) = { 𝑁 } } = { 𝑥 ∣ ( 𝑥 ∈ dom 𝐽 ∧ ( ( iEdg ‘ 𝑈 ) ‘ 𝑥 ) = { 𝑁 } ) }
86	47	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐽 ) → ( ( ( iEdg ‘ 𝑈 ) ‘ 𝑥 ) = { 𝑁 } ↔ ( 𝐽 ‘ 𝑥 ) = { 𝑁 } ) )
87	86	rabbidva	⊢ ( 𝜑 → { 𝑥 ∈ dom 𝐽 ∣ ( ( iEdg ‘ 𝑈 ) ‘ 𝑥 ) = { 𝑁 } } = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) = { 𝑁 } } )
88	85 87	eqtr3id	⊢ ( 𝜑 → { 𝑥 ∣ ( 𝑥 ∈ 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 ‘ 𝐻 ) ‘ 𝑁 ) ) )