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=\mathrm{Vtx}\left(G\right)$$
	vdegp1ai.u	$$⊢U\in V$$
	vdegp1ai.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	vdegp1ai.w	$$⊢I\in \mathrm{Word}\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
	vdegp1ai.d	$$⊢\mathrm{VtxDeg}\left(G\right)\left(U\right)=P$$
	vdegp1ai.vf	$$⊢\mathrm{Vtx}\left(F\right)=V$$
	vdegp1bi.x	$$⊢X\in V$$
	vdegp1bi.xu	$$⊢X\ne U$$
	vdegp1ci.f	$$⊢\mathrm{iEdg}\left(F\right)=I\mathrm{++}⟨“\left\{X,U\right\}”⟩$$
Assertion	vdegp1ci	$$⊢\mathrm{VtxDeg}\left(F\right)\left(U\right)=P+1$$

Proof

Step	Hyp	Ref	Expression
1		vdegp1ai.vg	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		vdegp1ai.u	$$⊢U\in V$$
3		vdegp1ai.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
4		vdegp1ai.w	$$⊢I\in \mathrm{Word}\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
5		vdegp1ai.d	$$⊢\mathrm{VtxDeg}\left(G\right)\left(U\right)=P$$
6		vdegp1ai.vf	$$⊢\mathrm{Vtx}\left(F\right)=V$$
7		vdegp1bi.x	$$⊢X\in V$$
8		vdegp1bi.xu	$$⊢X\ne U$$
9		vdegp1ci.f	$$⊢\mathrm{iEdg}\left(F\right)=I\mathrm{++}⟨“\left\{X,U\right\}”⟩$$
10		prcom	$$⊢\left\{X,U\right\}=\left\{U,X\right\}$$
11		s1eq	$$⊢\left\{X,U\right\}=\left\{U,X\right\}\to ⟨“\left\{X,U\right\}”⟩=⟨“\left\{U,X\right\}”⟩$$
12	10 11	ax-mp	$$⊢⟨“\left\{X,U\right\}”⟩=⟨“\left\{U,X\right\}”⟩$$
13	12	oveq2i	$$⊢I\mathrm{++}⟨“\left\{X,U\right\}”⟩=I\mathrm{++}⟨“\left\{U,X\right\}”⟩$$
14	9 13	eqtri	$$⊢\mathrm{iEdg}\left(F\right)=I\mathrm{++}⟨“\left\{U,X\right\}”⟩$$
15	1 2 3 4 5 6 7 8 14	vdegp1bi	$$⊢\mathrm{VtxDeg}\left(F\right)\left(U\right)=P+1$$