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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdginducedm1.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
vtxdginducedm1.k ⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
vtxdginducedm1.i ⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
vtxdginducedm1.p ⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
vtxdginducedm1.s ⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
vtxdginducedm1.j ⊢ 𝐽 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) }
Assertion vtxdginducedm1 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) )

Proof

Step Hyp Ref Expression
1 vtxdginducedm1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdginducedm1.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 vtxdginducedm1.k ⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
4 vtxdginducedm1.i ⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
5 vtxdginducedm1.p ⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
6 vtxdginducedm1.s ⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
7 vtxdginducedm1.j ⊢ 𝐽 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) }
8 7 4 elnelun ⊢ ( 𝐽 ∪ 𝐼 ) = dom 𝐸
9 8 eqcomi ⊢ dom 𝐸 = ( 𝐽 ∪ 𝐼 )
10 9 rabeqi ⊢ { 𝑘 ∈ dom 𝐸 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } = { 𝑘 ∈ ( 𝐽 ∪ 𝐼 ) ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) }
11 rabun2 ⊢ { 𝑘 ∈ ( 𝐽 ∪ 𝐼 ) ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } = ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∪ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } )
12 10 11 eqtri ⊢ { 𝑘 ∈ dom 𝐸 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } = ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∪ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } )
13 12 fveq2i ⊢ ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) = ( ♯ ‘ ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∪ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) )
14 2 fvexi ⊢ 𝐸 ∈ V
15 14 dmex ⊢ dom 𝐸 ∈ V
16 7 15 rab2ex ⊢ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∈ V
17 4 15 rab2ex ⊢ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∈ V
18 ssrab2 ⊢ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ⊆ 𝐽
19 ssrab2 ⊢ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ⊆ 𝐼
20 ss2in ⊢ ( ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ⊆ 𝐽 ∧ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ⊆ 𝐼 ) → ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∩ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ⊆ ( 𝐽 ∩ 𝐼 ) )
21 18 19 20 mp2an ⊢ ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∩ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ⊆ ( 𝐽 ∩ 𝐼 )
22 7 4 elneldisj ⊢ ( 𝐽 ∩ 𝐼 ) = ∅
23 22 sseq2i ⊢ ( ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∩ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ⊆ ( 𝐽 ∩ 𝐼 ) ↔ ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∩ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ⊆ ∅ )
24 ss0 ⊢ ( ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∩ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ⊆ ∅ → ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∩ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) = ∅ )
25 23 24 sylbi ⊢ ( ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∩ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ⊆ ( 𝐽 ∩ 𝐼 ) → ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∩ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) = ∅ )
26 21 25 ax-mp ⊢ ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∩ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) = ∅
27 hashunx ⊢ ( ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∈ V ∧ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∈ V ∧ ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∩ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) = ∅ ) → ( ♯ ‘ ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∪ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ) = ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ) )
28 16 17 26 27 mp3an ⊢ ( ♯ ‘ ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∪ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ) = ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) )
29 13 28 eqtri ⊢ ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) = ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) )
30 9 rabeqi ⊢ { 𝑘 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } = { 𝑘 ∈ ( 𝐽 ∪ 𝐼 ) ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } }
31 rabun2 ⊢ { 𝑘 ∈ ( 𝐽 ∪ 𝐼 ) ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } = ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∪ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } )
32 30 31 eqtri ⊢ { 𝑘 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } = ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∪ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } )
33 32 fveq2i ⊢ ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) = ( ♯ ‘ ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∪ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) )
34 7 15 rab2ex ⊢ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∈ V
35 4 15 rab2ex ⊢ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∈ V
36 ssrab2 ⊢ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ⊆ 𝐽
37 ssrab2 ⊢ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ⊆ 𝐼
38 ss2in ⊢ ( ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ⊆ 𝐽 ∧ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ⊆ 𝐼 ) → ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∩ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ⊆ ( 𝐽 ∩ 𝐼 ) )
39 36 37 38 mp2an ⊢ ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∩ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ⊆ ( 𝐽 ∩ 𝐼 )
40 22 sseq2i ⊢ ( ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∩ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ⊆ ( 𝐽 ∩ 𝐼 ) ↔ ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∩ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ⊆ ∅ )
41 ss0 ⊢ ( ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∩ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ⊆ ∅ → ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∩ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) = ∅ )
42 40 41 sylbi ⊢ ( ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∩ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ⊆ ( 𝐽 ∩ 𝐼 ) → ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∩ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) = ∅ )
43 39 42 ax-mp ⊢ ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∩ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) = ∅
44 hashunx ⊢ ( ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∈ V ∧ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∈ V ∧ ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∩ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) = ∅ ) → ( ♯ ‘ ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∪ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) = ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) )
45 34 35 43 44 mp3an ⊢ ( ♯ ‘ ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∪ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) = ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) )
46 33 45 eqtri ⊢ ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) = ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) )
47 29 46 oveq12i ⊢ ( ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) = ( ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ) +𝑒 ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) )
48 hashxnn0 ⊢ ( { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∈ V → ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℕ0* )
49 16 48 ax-mp ⊢ ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℕ0*
50 49 a1i ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℕ0* )
51 hashxnn0 ⊢ ( { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ∈ V → ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℕ0* )
52 17 51 ax-mp ⊢ ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℕ0*
53 52 a1i ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℕ0* )
54 hashxnn0 ⊢ ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∈ V → ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ∈ ℕ0* )
55 34 54 ax-mp ⊢ ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ∈ ℕ0*
56 55 a1i ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ∈ ℕ0* )
57 hashxnn0 ⊢ ( { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ∈ V → ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ∈ ℕ0* )
58 35 57 ax-mp ⊢ ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ∈ ℕ0*
59 58 a1i ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ∈ ℕ0* )
60 50 53 56 59 xnn0add4d ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ) +𝑒 ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ) = ( ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ) )
61 xnn0xaddcl ⊢ ( ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℕ0* ∧ ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ∈ ℕ0* ) → ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℕ0* )
62 49 55 61 mp2an ⊢ ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℕ0*
63 xnn0xr ⊢ ( ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℕ0* → ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℝ* )
64 62 63 ax-mp ⊢ ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℝ*
65 xnn0xaddcl ⊢ ( ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℕ0* ∧ ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ∈ ℕ0* ) → ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℕ0* )
66 52 58 65 mp2an ⊢ ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℕ0*
67 xnn0xr ⊢ ( ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℕ0* → ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℝ* )
68 66 67 ax-mp ⊢ ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℝ*
69 xaddcom ⊢ ( ( ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℝ* ∧ ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ∈ ℝ* ) → ( ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ) = ( ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ) )
70 64 68 69 mp2an ⊢ ( ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ) = ( ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) )
71 1 2 3 4 5 6 7 vtxdginducedm1lem4 ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) = 0 )
72 71 oveq2d ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) = ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 0 ) )
73 xnn0xr ⊢ ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℕ0* → ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℝ* )
74 49 73 ax-mp ⊢ ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℝ*
75 xaddid1 ⊢ ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ∈ ℝ* → ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 0 ) = ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) )
76 74 75 ax-mp ⊢ ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 0 ) = ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } )
77 72 76 eqtrdi ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) = ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) )
78 fveq2 ⊢ ( 𝑘 = 𝑙 → ( 𝐸 ‘ 𝑘 ) = ( 𝐸 ‘ 𝑙 ) )
79 78 eleq2d ⊢ ( 𝑘 = 𝑙 → ( 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) ↔ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) ) )
80 79 cbvrabv ⊢ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } = { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) }
81 80 fveq2i ⊢ ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) = ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } )
82 77 81 eqtrdi ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) = ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) )
83 82 oveq2d ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ) = ( ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) )
84 70 83 syl5eq ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ) = ( ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) )
85 60 84 eqtrd ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) ) +𝑒 ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) ) = ( ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) )
86 47 85 syl5eq ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) = ( ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) )
87 1 2 3 4 5 6 vtxdginducedm1lem2 ⊢ dom ( iEdg ‘ 𝑆 ) = 𝐼
88 87 rabeqi ⊢ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) } = { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) }
89 1 2 3 4 5 6 vtxdginducedm1lem3 ⊢ ( 𝑘 ∈ 𝐼 → ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = ( 𝐸 ‘ 𝑘 ) )
90 89 eleq2d ⊢ ( 𝑘 ∈ 𝐼 → ( 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) ↔ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) ) )
91 90 rabbiia ⊢ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) } = { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) }
92 88 91 eqtri ⊢ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) } = { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) }
93 92 fveq2i ⊢ ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) } ) = ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } )
94 87 rabeqi ⊢ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } } = { 𝑘 ∈ 𝐼 ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } }
95 89 eqeq1d ⊢ ( 𝑘 ∈ 𝐼 → ( ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } ↔ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } ) )
96 95 rabbiia ⊢ { 𝑘 ∈ 𝐼 ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } } = { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } }
97 94 96 eqtri ⊢ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } } = { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } }
98 97 fveq2i ⊢ ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } } ) = ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } )
99 93 98 oveq12i ⊢ ( ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } } ) ) = ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) )
100 99 eqcomi ⊢ ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) = ( ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } } ) )
101 100 oveq1i ⊢ ( ( ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ 𝐼 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) = ( ( ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) )
102 86 101 eqtrdi ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) = ( ( ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) )
103 eldifi ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑣 ∈ 𝑉 )
104 eqid ⊢ dom 𝐸 = dom 𝐸
105 1 2 104 vtxdgval ⊢ ( 𝑣 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) )
106 103 105 syl ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑣 } } ) ) )
107 6 fveq2i ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ ⟨ 𝐾 , 𝑃 ⟩ )
108 1 fvexi ⊢ 𝑉 ∈ V
109 difexg ⊢ ( 𝑉 ∈ V → ( 𝑉 ∖ { 𝑁 } ) ∈ V )
110 3 109 eqeltrid ⊢ ( 𝑉 ∈ V → 𝐾 ∈ V )
111 108 110 ax-mp ⊢ 𝐾 ∈ V
112 resexg ⊢ ( 𝐸 ∈ V → ( 𝐸 ↾ 𝐼 ) ∈ V )
113 5 112 eqeltrid ⊢ ( 𝐸 ∈ V → 𝑃 ∈ V )
114 14 113 ax-mp ⊢ 𝑃 ∈ V
115 111 114 opvtxfvi ⊢ ( Vtx ‘ ⟨ 𝐾 , 𝑃 ⟩ ) = 𝐾
116 107 115 eqtri ⊢ ( Vtx ‘ 𝑆 ) = 𝐾
117 116 eleq2i ⊢ ( 𝑣 ∈ ( Vtx ‘ 𝑆 ) ↔ 𝑣 ∈ 𝐾 )
118 3 eleq2i ⊢ ( 𝑣 ∈ 𝐾 ↔ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) )
119 117 118 sylbbr ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑣 ∈ ( Vtx ‘ 𝑆 ) )
120 eqid ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 )
121 eqid ⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 )
122 eqid ⊢ dom ( iEdg ‘ 𝑆 ) = dom ( iEdg ‘ 𝑆 )
123 120 121 122 vtxdgval ⊢ ( 𝑣 ∈ ( Vtx ‘ 𝑆 ) → ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } } ) ) )
124 119 123 syl ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } } ) ) )
125 124 oveq1d ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) = ( ( ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ 𝑣 ∈ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) } ) +𝑒 ( ♯ ‘ { 𝑘 ∈ dom ( iEdg ‘ 𝑆 ) ∣ ( ( iEdg ‘ 𝑆 ) ‘ 𝑘 ) = { 𝑣 } } ) ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) )
126 102 106 125 3eqtr4d ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) )
127 126 rgen ⊢ ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) )