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 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 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 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 ‘ 𝐻 ) ‘ 𝑁 ) ) )