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 e. V
	vdegp1ai.i	|- I = ( iEdg ` G )
	vdegp1ai.w	|- I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 }
	vdegp1ai.d	|- ( ( VtxDeg ` G ) ` U ) = P
	vdegp1ai.vf	|- ( Vtx ` F ) = V
	vdegp1bi.x	|- X e. 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 e. V
3		vdegp1ai.i	|- I = ( iEdg ` G )
4		vdegp1ai.w	|- I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 }
5		vdegp1ai.d	|- ( ( VtxDeg ` G ) ` U ) = P
6		vdegp1ai.vf	|- ( Vtx ` F ) = V
7		vdegp1bi.x	|- X e. 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 )