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 |
|
vdegp1ci.f |
β’ ( iEdg β πΉ ) = ( πΌ ++ β¨β { π , π } ββ© ) |
10 |
|
prcom |
β’ { π , π } = { π , π } |
11 |
|
s1eq |
β’ ( { π , π } = { π , π } β β¨β { π , π } ββ© = β¨β { π , π } ββ© ) |
12 |
10 11
|
ax-mp |
β’ β¨β { π , π } ββ© = β¨β { π , π } ββ© |
13 |
12
|
oveq2i |
β’ ( πΌ ++ β¨β { π , π } ββ© ) = ( πΌ ++ β¨β { π , π } ββ© ) |
14 |
9 13
|
eqtri |
β’ ( iEdg β πΉ ) = ( πΌ ++ β¨β { π , π } ββ© ) |
15 |
1 2 3 4 5 6 7 8 14
|
vdegp1bi |
β’ ( ( VtxDeg β πΉ ) β π ) = ( π + 1 ) |