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 ⊒ 𝑉 = ( 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 eqtrid ⊒ ( { π‘ˆ , 𝑋 } ∈ 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 )