This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → 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