Metamath Proof Explorer


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 = Vtx G
vdegp1ai.u U V
vdegp1ai.i I = iEdg G
vdegp1ai.w I Word x 𝒫 V | x 2
vdegp1ai.d VtxDeg G U = P
vdegp1ai.vf Vtx F = V
vdegp1bi.x X V
vdegp1bi.xu X U
vdegp1bi.f iEdg F = I ++ ⟨“ U X ”⟩
Assertion vdegp1bi VtxDeg F U = P + 1

Proof

Step Hyp Ref Expression
1 vdegp1ai.vg V = Vtx G
2 vdegp1ai.u U V
3 vdegp1ai.i I = iEdg G
4 vdegp1ai.w I Word x 𝒫 V | x 2
5 vdegp1ai.d VtxDeg G U = P
6 vdegp1ai.vf Vtx F = V
7 vdegp1bi.x X V
8 vdegp1bi.xu X U
9 vdegp1bi.f iEdg F = I ++ ⟨“ U X ”⟩
10 prex U X V
11 wrdf I Word x 𝒫 V | x 2 I : 0 ..^ I x 𝒫 V | x 2
12 11 ffund I Word x 𝒫 V | x 2 Fun I
13 4 12 mp1i U X V Fun I
14 6 a1i U X V Vtx F = V
15 wrdv I Word x 𝒫 V | x 2 I Word V
16 4 15 ax-mp I Word V
17 cats1un I Word V U X V I ++ ⟨“ U X ”⟩ = I I U X
18 16 17 mpan U X V I ++ ⟨“ U X ”⟩ = I I U X
19 9 18 syl5eq U X V iEdg F = I I U X
20 fvexd U X V I V
21 wrdlndm I Word x 𝒫 V | x 2 I dom I
22 4 21 mp1i U X V I dom I
23 2 a1i U X V U V
24 2 7 pm3.2i U V X V
25 prelpwi U V X V U X 𝒫 V
26 24 25 mp1i U X V U X 𝒫 V
27 prid1g U V U U X
28 2 27 mp1i U X V U U X
29 8 necomi U X
30 hashprg U V X V U X U X = 2
31 2 7 30 mp2an U X U X = 2
32 29 31 mpbi U X = 2
33 32 eqcomi 2 = U X
34 2re 2
35 34 eqlei 2 = U X 2 U X
36 33 35 mp1i U X V 2 U X
37 1 3 13 14 19 20 22 23 26 28 36 p1evtxdp1 U X V VtxDeg F U = VtxDeg G U + 𝑒 1
38 10 37 ax-mp VtxDeg F U = VtxDeg G U + 𝑒 1
39 fzofi 0 ..^ I Fin
40 wrddm I Word x 𝒫 V | x 2 dom I = 0 ..^ I
41 4 40 ax-mp dom I = 0 ..^ I
42 41 eqcomi 0 ..^ I = dom I
43 1 3 42 vtxdgfisnn0 0 ..^ I Fin U V VtxDeg G U 0
44 39 2 43 mp2an VtxDeg G U 0
45 44 nn0rei VtxDeg G U
46 1re 1
47 rexadd VtxDeg G U 1 VtxDeg G U + 𝑒 1 = VtxDeg G U + 1
48 45 46 47 mp2an VtxDeg G U + 𝑒 1 = VtxDeg G U + 1
49 5 oveq1i VtxDeg G U + 1 = P + 1
50 38 48 49 3eqtri VtxDeg F U = P + 1