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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vdegp1ai.u	⊢ 𝑈 ∈ 𝑉
	vdegp1ai.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	vdegp1ai.w	⊢ 𝐼 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
	vdegp1ai.d	⊢ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 𝑃
	vdegp1ai.vf	⊢ ( Vtx ‘ 𝐹 ) = 𝑉
	vdegp1ai.x	⊢ 𝑋 ∈ 𝑉
	vdegp1ai.xu	⊢ 𝑋 ≠ 𝑈
	vdegp1ai.y	⊢ 𝑌 ∈ 𝑉
	vdegp1ai.yu	⊢ 𝑌 ≠ 𝑈
	vdegp1ai.f	⊢ ( iEdg ‘ 𝐹 ) = ( 𝐼 ++ ⟨“ { 𝑋 , 𝑌 } ”⟩ )
Assertion	vdegp1ai	⊢ ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = 𝑃

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		vdegp1ai.x	⊢ 𝑋 ∈ 𝑉
8		vdegp1ai.xu	⊢ 𝑋 ≠ 𝑈
9		vdegp1ai.y	⊢ 𝑌 ∈ 𝑉
10		vdegp1ai.yu	⊢ 𝑌 ≠ 𝑈
11		vdegp1ai.f	⊢ ( iEdg ‘ 𝐹 ) = ( 𝐼 ++ ⟨“ { 𝑋 , 𝑌 } ”⟩ )
12		prex	⊢ { 𝑋 , 𝑌 } ∈ V
13		wrdf	⊢ ( 𝐼 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → 𝐼 : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
14	13	ffund	⊢ ( 𝐼 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → Fun 𝐼 )
15	4 14	mp1i	⊢ ( { 𝑋 , 𝑌 } ∈ V → Fun 𝐼 )
16	6	a1i	⊢ ( { 𝑋 , 𝑌 } ∈ V → ( Vtx ‘ 𝐹 ) = 𝑉 )
17		wrdv	⊢ ( 𝐼 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → 𝐼 ∈ Word V )
18	4 17	ax-mp	⊢ 𝐼 ∈ Word V
19		cats1un	⊢ ( ( 𝐼 ∈ Word V ∧ { 𝑋 , 𝑌 } ∈ V ) → ( 𝐼 ++ ⟨“ { 𝑋 , 𝑌 } ”⟩ ) = ( 𝐼 ∪ { ⟨ ( ♯ ‘ 𝐼 ) , { 𝑋 , 𝑌 } ⟩ } ) )
20	18 19	mpan	⊢ ( { 𝑋 , 𝑌 } ∈ V → ( 𝐼 ++ ⟨“ { 𝑋 , 𝑌 } ”⟩ ) = ( 𝐼 ∪ { ⟨ ( ♯ ‘ 𝐼 ) , { 𝑋 , 𝑌 } ⟩ } ) )
21	11 20	eqtrid	⊢ ( { 𝑋 , 𝑌 } ∈ V → ( iEdg ‘ 𝐹 ) = ( 𝐼 ∪ { ⟨ ( ♯ ‘ 𝐼 ) , { 𝑋 , 𝑌 } ⟩ } ) )
22		fvexd	⊢ ( { 𝑋 , 𝑌 } ∈ V → ( ♯ ‘ 𝐼 ) ∈ V )
23		wrdlndm	⊢ ( 𝐼 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ( ♯ ‘ 𝐼 ) ∉ dom 𝐼 )
24	4 23	mp1i	⊢ ( { 𝑋 , 𝑌 } ∈ V → ( ♯ ‘ 𝐼 ) ∉ dom 𝐼 )
25	2	a1i	⊢ ( { 𝑋 , 𝑌 } ∈ V → 𝑈 ∈ 𝑉 )
26		id	⊢ ( { 𝑋 , 𝑌 } ∈ V → { 𝑋 , 𝑌 } ∈ V )
27	8	necomi	⊢ 𝑈 ≠ 𝑋
28	10	necomi	⊢ 𝑈 ≠ 𝑌
29	27 28	prneli	⊢ 𝑈 ∉ { 𝑋 , 𝑌 }
30	29	a1i	⊢ ( { 𝑋 , 𝑌 } ∈ V → 𝑈 ∉ { 𝑋 , 𝑌 } )
31	1 3 15 16 21 22 24 25 26 30	p1evtxdeq	⊢ ( { 𝑋 , 𝑌 } ∈ V → ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) )
32	12 31	ax-mp	⊢ ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 )
33	32 5	eqtri	⊢ ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = 𝑃