This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 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
vdegp1ai.x ⊢ X ∈ V
vdegp1ai.xu ⊢ X ≠ U
vdegp1ai.y ⊢ Y ∈ V
vdegp1ai.yu ⊢ Y ≠ U
vdegp1ai.f ⊢ iEdg ⁡ F = I ++ ⟨“ X Y ”⟩
Assertion vdegp1ai ⊢ VtxDeg ⁡ F ⁡ U = P

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 vdegp1ai.x ⊢ X ∈ V
8 vdegp1ai.xu ⊢ X ≠ U
9 vdegp1ai.y ⊢ Y ∈ V
10 vdegp1ai.yu ⊢ Y ≠ U
11 vdegp1ai.f ⊢ iEdg ⁡ F = I ++ ⟨“ X Y ”⟩
12 prex ⊢ X Y ∈ V
13 wrdf ⊢ I ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2 → I : 0 ..^ I ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
14 13 ffund ⊢ I ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2 → Fun ⁡ I
15 4 14 mp1i ⊢ X Y ∈ V → Fun ⁡ I
16 6 a1i ⊢ X Y ∈ V → Vtx ⁡ F = V
17 wrdv ⊢ I ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2 → I ∈ Word V
18 4 17 ax-mp ⊢ I ∈ Word V
19 cats1un ⊢ I ∈ Word V ∧ X Y ∈ V → I ++ ⟨“ X Y ”⟩ = I ∪ I X Y
20 18 19 mpan ⊢ X Y ∈ V → I ++ ⟨“ X Y ”⟩ = I ∪ I X Y
21 11 20 eqtrid ⊢ X Y ∈ V → iEdg ⁡ F = I ∪ I X Y
22 fvexd ⊢ X Y ∈ V → I ∈ V
23 wrdlndm ⊢ I ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2 → I ∉ dom ⁡ I
24 4 23 mp1i ⊢ X Y ∈ V → I ∉ dom ⁡ I
25 2 a1i ⊢ X Y ∈ V → U ∈ V
26 id ⊢ X Y ∈ V → X Y ∈ V
27 8 necomi ⊢ U ≠ X
28 10 necomi ⊢ U ≠ Y
29 27 28 prneli ⊢ U ∉ X Y
30 29 a1i ⊢ X Y ∈ V → U ∉ X Y
31 1 3 15 16 21 22 24 25 26 30 p1evtxdeq ⊢ X Y ∈ V → VtxDeg ⁡ F ⁡ U = VtxDeg ⁡ G ⁡ U
32 12 31 ax-mp ⊢ VtxDeg ⁡ F ⁡ U = VtxDeg ⁡ G ⁡ U
33 32 5 eqtri ⊢ VtxDeg ⁡ F ⁡ U = P