Metamath Proof Explorer


Theorem 1hegrvtxdg1

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 )