Database
GRAPH THEORY
Undirected graphs
Vertex degree
1hegrvtxdg1r
Metamath Proof Explorer
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