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 )