Metamath Proof Explorer


Theorem 1hegrvtxdg1r

Description: The vertex degree of a graph with one hyperedge, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 22-Dec-2017) (Revised by AV, 23-Feb-2021)

Ref Expression
Hypotheses 1hegrvtxdg1.a φ A X
1hegrvtxdg1.b φ B V
1hegrvtxdg1.c φ C V
1hegrvtxdg1.n φ B C
1hegrvtxdg1.x φ E 𝒫 V
1hegrvtxdg1.i φ iEdg G = A E
1hegrvtxdg1.e φ B C E
1hegrvtxdg1.v φ Vtx G = V
Assertion 1hegrvtxdg1r φ VtxDeg G C = 1

Proof

Step Hyp Ref Expression
1 1hegrvtxdg1.a φ A X
2 1hegrvtxdg1.b φ B V
3 1hegrvtxdg1.c φ C V
4 1hegrvtxdg1.n φ B C
5 1hegrvtxdg1.x φ E 𝒫 V
6 1hegrvtxdg1.i φ iEdg G = A E
7 1hegrvtxdg1.e φ B C E
8 1hegrvtxdg1.v φ Vtx G = V
9 4 necomd φ C B
10 prcom C B = B C
11 10 7 eqsstrid φ C B E
12 1 3 2 9 5 6 11 8 1hegrvtxdg1 φ VtxDeg G C = 1