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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vdegp1ai.u	⊢ 𝑈 ∈ 𝑉
	vdegp1ai.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	vdegp1ai.w	⊢ 𝐼 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
	vdegp1ai.d	⊢ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 𝑃
	vdegp1ai.vf	⊢ ( Vtx ‘ 𝐹 ) = 𝑉
	vdegp1bi.x	⊢ 𝑋 ∈ 𝑉
	vdegp1bi.xu	⊢ 𝑋 ≠ 𝑈
	vdegp1bi.f	⊢ ( iEdg ‘ 𝐹 ) = ( 𝐼 ++ ⟨“ { 𝑈 , 𝑋 } ”⟩ )
Assertion	vdegp1bi	⊢ ( ( 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		vdegp1bi.f	⊢ ( iEdg ‘ 𝐹 ) = ( 𝐼 ++ ⟨“ { 𝑈 , 𝑋 } ”⟩ )
10		prex	⊢ { 𝑈 , 𝑋 } ∈ V
11		wrdf	⊢ ( 𝐼 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → 𝐼 : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
12	11	ffund	⊢ ( 𝐼 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → Fun 𝐼 )
13	4 12	mp1i	⊢ ( { 𝑈 , 𝑋 } ∈ V → Fun 𝐼 )
14	6	a1i	⊢ ( { 𝑈 , 𝑋 } ∈ V → ( Vtx ‘ 𝐹 ) = 𝑉 )
15		wrdv	⊢ ( 𝐼 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → 𝐼 ∈ Word V )
16	4 15	ax-mp	⊢ 𝐼 ∈ Word V
17		cats1un	⊢ ( ( 𝐼 ∈ Word V ∧ { 𝑈 , 𝑋 } ∈ V ) → ( 𝐼 ++ ⟨“ { 𝑈 , 𝑋 } ”⟩ ) = ( 𝐼 ∪ { ⟨ ( ♯ ‘ 𝐼 ) , { 𝑈 , 𝑋 } ⟩ } ) )
18	16 17	mpan	⊢ ( { 𝑈 , 𝑋 } ∈ V → ( 𝐼 ++ ⟨“ { 𝑈 , 𝑋 } ”⟩ ) = ( 𝐼 ∪ { ⟨ ( ♯ ‘ 𝐼 ) , { 𝑈 , 𝑋 } ⟩ } ) )
19	9 18	syl5eq	⊢ ( { 𝑈 , 𝑋 } ∈ V → ( iEdg ‘ 𝐹 ) = ( 𝐼 ∪ { ⟨ ( ♯ ‘ 𝐼 ) , { 𝑈 , 𝑋 } ⟩ } ) )
20		fvexd	⊢ ( { 𝑈 , 𝑋 } ∈ V → ( ♯ ‘ 𝐼 ) ∈ V )
21		wrdlndm	⊢ ( 𝐼 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ( ♯ ‘ 𝐼 ) ∉ dom 𝐼 )
22	4 21	mp1i	⊢ ( { 𝑈 , 𝑋 } ∈ V → ( ♯ ‘ 𝐼 ) ∉ dom 𝐼 )
23	2	a1i	⊢ ( { 𝑈 , 𝑋 } ∈ V → 𝑈 ∈ 𝑉 )
24	2 7	pm3.2i	⊢ ( 𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 )
25		prelpwi	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → { 𝑈 , 𝑋 } ∈ 𝒫 𝑉 )
26	24 25	mp1i	⊢ ( { 𝑈 , 𝑋 } ∈ V → { 𝑈 , 𝑋 } ∈ 𝒫 𝑉 )
27		prid1g	⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ { 𝑈 , 𝑋 } )
28	2 27	mp1i	⊢ ( { 𝑈 , 𝑋 } ∈ V → 𝑈 ∈ { 𝑈 , 𝑋 } )
29	8	necomi	⊢ 𝑈 ≠ 𝑋
30		hashprg	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑈 ≠ 𝑋 ↔ ( ♯ ‘ { 𝑈 , 𝑋 } ) = 2 ) )
31	2 7 30	mp2an	⊢ ( 𝑈 ≠ 𝑋 ↔ ( ♯ ‘ { 𝑈 , 𝑋 } ) = 2 )
32	29 31	mpbi	⊢ ( ♯ ‘ { 𝑈 , 𝑋 } ) = 2
33	32	eqcomi	⊢ 2 = ( ♯ ‘ { 𝑈 , 𝑋 } )
34		2re	⊢ 2 ∈ ℝ
35	34	eqlei	⊢ ( 2 = ( ♯ ‘ { 𝑈 , 𝑋 } ) → 2 ≤ ( ♯ ‘ { 𝑈 , 𝑋 } ) )
36	33 35	mp1i	⊢ ( { 𝑈 , 𝑋 } ∈ V → 2 ≤ ( ♯ ‘ { 𝑈 , 𝑋 } ) )
37	1 3 13 14 19 20 22 23 26 28 36	p1evtxdp1	⊢ ( { 𝑈 , 𝑋 } ∈ V → ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +𝑒 1 ) )
38	10 37	ax-mp	⊢ ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +𝑒 1 )
39		fzofi	⊢ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ∈ Fin
40		wrddm	⊢ ( 𝐼 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → dom 𝐼 = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
41	4 40	ax-mp	⊢ dom 𝐼 = ( 0 ..^ ( ♯ ‘ 𝐼 ) )
42	41	eqcomi	⊢ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) = dom 𝐼
43	1 3 42	vtxdgfisnn0	⊢ ( ( ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ∈ ℕ0 )
44	39 2 43	mp2an	⊢ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ∈ ℕ0
45	44	nn0rei	⊢ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ∈ ℝ
46		1re	⊢ 1 ∈ ℝ
47		rexadd	⊢ ( ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +𝑒 1 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) + 1 ) )
48	45 46 47	mp2an	⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +𝑒 1 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) + 1 )
49	5	oveq1i	⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) + 1 ) = ( 𝑃 + 1 )
50	38 48 49	3eqtri	⊢ ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( 𝑃 + 1 )