This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vdegp1ci

Description: The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of U in the edge set E is P , then adding { X , U } to the edge set, where X =/= U , yields degree P + 1 . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Revised by AV, 3-Mar-2021)

Ref Expression
Hypotheses vdegp1ai.vg ⊢ V = Vtx ⁡ G
vdegp1ai.u ⊢ U ∈ V
vdegp1ai.i ⊢ I = iEdg ⁡ G
vdegp1ai.w ⊢ I ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2
vdegp1ai.d ⊢ VtxDeg ⁡ G ⁡ U = P
vdegp1ai.vf ⊢ Vtx ⁡ F = V
vdegp1bi.x ⊢ X ∈ V
vdegp1bi.xu ⊢ X ≠ U
vdegp1ci.f ⊢ iEdg ⁡ F = I ++ ⟨“ X U ”⟩
Assertion vdegp1ci ⊢ VtxDeg ⁡ F ⁡ U = P + 1

Proof

Step Hyp Ref Expression
1 vdegp1ai.vg ⊢ V = Vtx ⁡ G
2 vdegp1ai.u ⊢ U ∈ V
3 vdegp1ai.i ⊢ I = iEdg ⁡ G
4 vdegp1ai.w ⊢ I ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2
5 vdegp1ai.d ⊢ VtxDeg ⁡ G ⁡ U = P
6 vdegp1ai.vf ⊢ Vtx ⁡ F = V
7 vdegp1bi.x ⊢ X ∈ V
8 vdegp1bi.xu ⊢ X ≠ U
9 vdegp1ci.f ⊢ iEdg ⁡ F = I ++ ⟨“ X U ”⟩
10 prcom ⊢ X U = U X
11 s1eq ⊢ X U = U X → ⟨“ X U ”⟩ = ⟨“ U X ”⟩
12 10 11 ax-mp ⊢ ⟨“ X U ”⟩ = ⟨“ U X ”⟩
13 12 oveq2i ⊢ I ++ ⟨“ X U ”⟩ = I ++ ⟨“ U X ”⟩
14 9 13 eqtri ⊢ iEdg ⁡ F = I ++ ⟨“ U X ”⟩
15 1 2 3 4 5 6 7 8 14 vdegp1bi ⊢ VtxDeg ⁡ F ⁡ U = P + 1