Theorem vdegp1bi

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 { U , X } 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$$
	vdegp1bi.f	$$⊢\mathrm{iEdg}\left(F\right)=I\mathrm{++}⟨“\left\{U,X\right\}”⟩$$
Assertion	vdegp1bi	$$⊢\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		vdegp1bi.f	$$⊢\mathrm{iEdg}\left(F\right)=I\mathrm{++}⟨“\left\{U,X\right\}”⟩$$
10		prex	$$⊢\left\{U,X\right\}\in \mathrm{V}$$
11		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\}$$
12	11	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$$
13	4 12	mp1i	$$⊢\left\{U,X\right\}\in \mathrm{V}\to \mathrm{Fun}I$$
14	6	a1i	$$⊢\left\{U,X\right\}\in \mathrm{V}\to \mathrm{Vtx}\left(F\right)=V$$
15		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}$$
16	4 15	ax-mp	$$⊢I\in \mathrm{Word}\mathrm{V}$$
17		cats1un	$$⊢\left(I\in \mathrm{Word}\mathrm{V}\wedge \left\{U,X\right\}\in \mathrm{V}\right)\to I\mathrm{++}⟨“\left\{U,X\right\}”⟩=I\cup \left\{⟨\left|I\right|,\left\{U,X\right\}⟩\right\}$$
18	16 17	mpan	$$⊢\left\{U,X\right\}\in \mathrm{V}\to I\mathrm{++}⟨“\left\{U,X\right\}”⟩=I\cup \left\{⟨\left|I\right|,\left\{U,X\right\}⟩\right\}$$
19	9 18	eqtrid	$$⊢\left\{U,X\right\}\in \mathrm{V}\to \mathrm{iEdg}\left(F\right)=I\cup \left\{⟨\left|I\right|,\left\{U,X\right\}⟩\right\}$$
20		fvexd	$$⊢\left\{U,X\right\}\in \mathrm{V}\to \left|I\right|\in \mathrm{V}$$
21		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$$
22	4 21	mp1i	$$⊢\left\{U,X\right\}\in \mathrm{V}\to \left|I\right|\notin \mathrm{dom}I$$
23	2	a1i	$$⊢\left\{U,X\right\}\in \mathrm{V}\to U\in V$$
24	2 7	pm3.2i	$$⊢\left(U\in V\wedge X\in V\right)$$
25		prelpwi	$$⊢\left(U\in V\wedge X\in V\right)\to \left\{U,X\right\}\in 𝒫V$$
26	24 25	mp1i	$$⊢\left\{U,X\right\}\in \mathrm{V}\to \left\{U,X\right\}\in 𝒫V$$
27		prid1g	$$⊢U\in V\to U\in \left\{U,X\right\}$$
28	2 27	mp1i	$$⊢\left\{U,X\right\}\in \mathrm{V}\to U\in \left\{U,X\right\}$$
29	8	necomi	$$⊢U\ne X$$
30		hashprg	$$⊢\left(U\in V\wedge X\in V\right)\to \left(U\ne X\leftrightarrow \left|\left\{U,X\right\}\right|=2\right)$$
31	2 7 30	mp2an	$$⊢U\ne X\leftrightarrow \left|\left\{U,X\right\}\right|=2$$
32	29 31	mpbi	$$⊢\left|\left\{U,X\right\}\right|=2$$
33	32	eqcomi	$$⊢2=\left|\left\{U,X\right\}\right|$$
34		2re	$$⊢2\in ℝ$$
35	34	eqlei	$$⊢2=\left|\left\{U,X\right\}\right|\to 2\le \left|\left\{U,X\right\}\right|$$
36	33 35	mp1i	$$⊢\left\{U,X\right\}\in \mathrm{V}\to 2\le \left|\left\{U,X\right\}\right|$$
37	1 3 13 14 19 20 22 23 26 28 36	p1evtxdp1	$$⊢\left\{U,X\right\}\in \mathrm{V}\to \mathrm{VtxDeg}\left(F\right)\left(U\right)=\mathrm{VtxDeg}\left(G\right)\left(U\right){+}_{𝑒}1$$
38	10 37	ax-mp	$$⊢\mathrm{VtxDeg}\left(F\right)\left(U\right)=\mathrm{VtxDeg}\left(G\right)\left(U\right){+}_{𝑒}1$$
39		fzofi	$$⊢\left(0..^\left|I\right|\right)\in \mathrm{Fin}$$
40		wrddm	$$⊢I\in \mathrm{Word}\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\to \mathrm{dom}I=\left(0..^\left|I\right|\right)$$
41	4 40	ax-mp	$$⊢\mathrm{dom}I=\left(0..^\left|I\right|\right)$$
42	41	eqcomi	$$⊢\left(0..^\left|I\right|\right)=\mathrm{dom}I$$
43	1 3 42	vtxdgfisnn0	$$⊢\left(\left(0..^\left|I\right|\right)\in \mathrm{Fin}\wedge U\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(U\right)\in {\mathbb{N}}_0$$
44	39 2 43	mp2an	$$⊢\mathrm{VtxDeg}\left(G\right)\left(U\right)\in {\mathbb{N}}_0$$
45	44	nn0rei	$$⊢\mathrm{VtxDeg}\left(G\right)\left(U\right)\in ℝ$$
46		1re	$$⊢1\in ℝ$$
47		rexadd	$$⊢\left(\mathrm{VtxDeg}\left(G\right)\left(U\right)\in ℝ\wedge 1\in ℝ\right)\to \mathrm{VtxDeg}\left(G\right)\left(U\right){+}_{𝑒}1=\mathrm{VtxDeg}\left(G\right)\left(U\right)+1$$
48	45 46 47	mp2an	$$⊢\mathrm{VtxDeg}\left(G\right)\left(U\right){+}_{𝑒}1=\mathrm{VtxDeg}\left(G\right)\left(U\right)+1$$
49	5	oveq1i	$$⊢\mathrm{VtxDeg}\left(G\right)\left(U\right)+1=P+1$$
50	38 48 49	3eqtri	$$⊢\mathrm{VtxDeg}\left(F\right)\left(U\right)=P+1$$