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
⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
1hegrvtxdg1.b
⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
1hegrvtxdg1.c
⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
1hegrvtxdg1.n
⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
1hegrvtxdg1.x
⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑉 )
1hegrvtxdg1.i
⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { 〈 𝐴 , 𝐸 〉 } )
1hegrvtxdg1.e
⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ 𝐸 )
1hegrvtxdg1.v
⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
Assertion
1hegrvtxdg1
⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐵 ) = 1 )
Proof
Step
Hyp
Ref
Expression
1
1hegrvtxdg1.a
⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
2
1hegrvtxdg1.b
⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3
1hegrvtxdg1.c
⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4
1hegrvtxdg1.n
⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
5
1hegrvtxdg1.x
⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑉 )
6
1hegrvtxdg1.i
⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { 〈 𝐴 , 𝐸 〉 } )
7
1hegrvtxdg1.e
⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ 𝐸 )
8
1hegrvtxdg1.v
⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
9
prid1g
⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ { 𝐵 , 𝐶 } )
10
2 9
syl
⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 , 𝐶 } )
11
7 10
sseldd
⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
12
prid2g
⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ { 𝐵 , 𝐶 } )
13
3 12
syl
⊢ ( 𝜑 → 𝐶 ∈ { 𝐵 , 𝐶 } )
14
7 13
sseldd
⊢ ( 𝜑 → 𝐶 ∈ 𝐸 )
15
5 11 14 4
nehash2
⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝐸 ) )
16
6 8 1 2 5 11 15
1hevtxdg1
⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐵 ) = 1 )