Theorem vdegp1ai

Description: The induction step for a vertex degree calculation. If the degree of U in the edge set E is P , then adding { X , Y } to the edge set, where X =/= U =/= Y , yields degree P as well. (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$$
	vdegp1ai.x	$$⊢X\in V$$
	vdegp1ai.xu	$$⊢X\ne U$$
	vdegp1ai.y	$$⊢Y\in V$$
	vdegp1ai.yu	$$⊢Y\ne U$$
	vdegp1ai.f	$$⊢\mathrm{iEdg}\left(F\right)=I\mathrm{++}⟨“\left\{X,Y\right\}”⟩$$
Assertion	vdegp1ai	$$⊢\mathrm{VtxDeg}\left(F\right)\left(U\right)=P$$

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		vdegp1ai.x	$$⊢X\in V$$
8		vdegp1ai.xu	$$⊢X\ne U$$
9		vdegp1ai.y	$$⊢Y\in V$$
10		vdegp1ai.yu	$$⊢Y\ne U$$
11		vdegp1ai.f	$$⊢\mathrm{iEdg}\left(F\right)=I\mathrm{++}⟨“\left\{X,Y\right\}”⟩$$
12		prex	$$⊢\left\{X,Y\right\}\in \mathrm{V}$$
13		wrdf	$$⊢I\in \mathrm{Word}\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\to I:\left(0..^\left|I\right|\right)⟶\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
14	13	ffund	$$⊢I\in \mathrm{Word}\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\to \mathrm{Fun}I$$
15	4 14	mp1i	$$⊢\left\{X,Y\right\}\in \mathrm{V}\to \mathrm{Fun}I$$
16	6	a1i	$$⊢\left\{X,Y\right\}\in \mathrm{V}\to \mathrm{Vtx}\left(F\right)=V$$
17		wrdv	$$⊢I\in \mathrm{Word}\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\to I\in \mathrm{Word}\mathrm{V}$$
18	4 17	ax-mp	$$⊢I\in \mathrm{Word}\mathrm{V}$$
19		cats1un	$$⊢\left(I\in \mathrm{Word}\mathrm{V}\wedge \left\{X,Y\right\}\in \mathrm{V}\right)\to I\mathrm{++}⟨“\left\{X,Y\right\}”⟩=I\cup \left\{⟨\left|I\right|,\left\{X,Y\right\}⟩\right\}$$
20	18 19	mpan	$$⊢\left\{X,Y\right\}\in \mathrm{V}\to I\mathrm{++}⟨“\left\{X,Y\right\}”⟩=I\cup \left\{⟨\left|I\right|,\left\{X,Y\right\}⟩\right\}$$
21	11 20	syl5eq	$$⊢\left\{X,Y\right\}\in \mathrm{V}\to \mathrm{iEdg}\left(F\right)=I\cup \left\{⟨\left|I\right|,\left\{X,Y\right\}⟩\right\}$$
22		fvexd	$$⊢\left\{X,Y\right\}\in \mathrm{V}\to \left|I\right|\in \mathrm{V}$$
23		wrdlndm	$$⊢I\in \mathrm{Word}\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\to \left|I\right|\notin \mathrm{dom}I$$
24	4 23	mp1i	$$⊢\left\{X,Y\right\}\in \mathrm{V}\to \left|I\right|\notin \mathrm{dom}I$$
25	2	a1i	$$⊢\left\{X,Y\right\}\in \mathrm{V}\to U\in V$$
26		id	$$⊢\left\{X,Y\right\}\in \mathrm{V}\to \left\{X,Y\right\}\in \mathrm{V}$$
27	8	necomi	$$⊢U\ne X$$
28	10	necomi	$$⊢U\ne Y$$
29	27 28	prneli	$$⊢U\notin \left\{X,Y\right\}$$
30	29	a1i	$$⊢\left\{X,Y\right\}\in \mathrm{V}\to U\notin \left\{X,Y\right\}$$
31	1 3 15 16 21 22 24 25 26 30	p1evtxdeq	$$⊢\left\{X,Y\right\}\in \mathrm{V}\to \mathrm{VtxDeg}\left(F\right)\left(U\right)=\mathrm{VtxDeg}\left(G\right)\left(U\right)$$
32	12 31	ax-mp	$$⊢\mathrm{VtxDeg}\left(F\right)\left(U\right)=\mathrm{VtxDeg}\left(G\right)\left(U\right)$$
33	32 5	eqtri	$$⊢\mathrm{VtxDeg}\left(F\right)\left(U\right)=P$$