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 ⊒ 𝑉 = ( Vtx β€˜ 𝐺 )
vdegp1ai.u ⊒ π‘ˆ ∈ 𝑉
vdegp1ai.i ⊒ 𝐼 = ( iEdg β€˜ 𝐺 )
vdegp1ai.w ⊒ 𝐼 ∈ Word { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) ≀ 2 }
vdegp1ai.d ⊒ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘ˆ ) = 𝑃
vdegp1ai.vf ⊒ ( Vtx β€˜ 𝐹 ) = 𝑉
vdegp1bi.x ⊒ 𝑋 ∈ 𝑉
vdegp1bi.xu ⊒ 𝑋 β‰  π‘ˆ
vdegp1ci.f ⊒ ( iEdg β€˜ 𝐹 ) = ( 𝐼 ++ βŸ¨β€œ { 𝑋 , π‘ˆ } β€βŸ© )
Assertion vdegp1ci ( ( VtxDeg β€˜ 𝐹 ) β€˜ π‘ˆ ) = ( 𝑃 + 1 )

Proof

Step Hyp Ref Expression
1 vdegp1ai.vg ⊒ 𝑉 = ( Vtx β€˜ 𝐺 )
2 vdegp1ai.u ⊒ π‘ˆ ∈ 𝑉
3 vdegp1ai.i ⊒ 𝐼 = ( iEdg β€˜ 𝐺 )
4 vdegp1ai.w ⊒ 𝐼 ∈ Word { π‘₯ ∈ ( 𝒫 𝑉 βˆ– { βˆ… } ) ∣ ( β™― β€˜ π‘₯ ) ≀ 2 }
5 vdegp1ai.d ⊒ ( ( VtxDeg β€˜ 𝐺 ) β€˜ π‘ˆ ) = 𝑃
6 vdegp1ai.vf ⊒ ( Vtx β€˜ 𝐹 ) = 𝑉
7 vdegp1bi.x ⊒ 𝑋 ∈ 𝑉
8 vdegp1bi.xu ⊒ 𝑋 β‰  π‘ˆ
9 vdegp1ci.f ⊒ ( iEdg β€˜ 𝐹 ) = ( 𝐼 ++ βŸ¨β€œ { 𝑋 , π‘ˆ } β€βŸ© )
10 prcom ⊒ { 𝑋 , π‘ˆ } = { π‘ˆ , 𝑋 }
11 s1eq ⊒ ( { 𝑋 , π‘ˆ } = { π‘ˆ , 𝑋 } β†’ βŸ¨β€œ { 𝑋 , π‘ˆ } β€βŸ© = βŸ¨β€œ { π‘ˆ , 𝑋 } β€βŸ© )
12 10 11 ax-mp ⊒ βŸ¨β€œ { 𝑋 , π‘ˆ } β€βŸ© = βŸ¨β€œ { π‘ˆ , 𝑋 } β€βŸ©
13 12 oveq2i ⊒ ( 𝐼 ++ βŸ¨β€œ { 𝑋 , π‘ˆ } β€βŸ© ) = ( 𝐼 ++ βŸ¨β€œ { π‘ˆ , 𝑋 } β€βŸ© )
14 9 13 eqtri ⊒ ( iEdg β€˜ 𝐹 ) = ( 𝐼 ++ βŸ¨β€œ { π‘ˆ , 𝑋 } β€βŸ© )
15 1 2 3 4 5 6 7 8 14 vdegp1bi ⊒ ( ( VtxDeg β€˜ 𝐹 ) β€˜ π‘ˆ ) = ( 𝑃 + 1 )