Database
GRAPH THEORY
Undirected graphs
Vertex degree
1hegrvtxdg1
Metamath Proof Explorer
Description: The vertex degree of a graph with one hyperedge, case 2: an edge from
the given vertex to some other 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
1hegrvtxdg1
⊢ φ → VtxDeg ⁡ G ⁡ B = 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
prid1g
⊢ B ∈ V → B ∈ B C
10
2 9
syl
⊢ φ → B ∈ B C
11
7 10
sseldd
⊢ φ → B ∈ E
12
prid2g
⊢ C ∈ V → C ∈ B C
13
3 12
syl
⊢ φ → C ∈ B C
14
7 13
sseldd
⊢ φ → C ∈ E
15
5 11 14 4
nehash2
⊢ φ → 2 ≤ E
16
6 8 1 2 5 11 15
1hevtxdg1
⊢ φ → VtxDeg ⁡ G ⁡ B = 1