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