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	$$⊢\phi \to A\in X$$
	1hegrvtxdg1.b	$$⊢\phi \to B\in V$$
	1hegrvtxdg1.c	$$⊢\phi \to C\in V$$
	1hegrvtxdg1.n	$$⊢\phi \to B\ne C$$
	1hegrvtxdg1.x	$$⊢\phi \to E\in 𝒫V$$
	1hegrvtxdg1.i	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,E⟩\right\}$$
	1hegrvtxdg1.e	$$⊢\phi \to \left\{B,C\right\}\subseteq E$$
	1hegrvtxdg1.v	$$⊢\phi \to \mathrm{Vtx}\left(G\right)=V$$
Assertion	1hegrvtxdg1	$$⊢\phi \to \mathrm{VtxDeg}\left(G\right)\left(B\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		1hegrvtxdg1.a	$$⊢\phi \to A\in X$$
2		1hegrvtxdg1.b	$$⊢\phi \to B\in V$$
3		1hegrvtxdg1.c	$$⊢\phi \to C\in V$$
4		1hegrvtxdg1.n	$$⊢\phi \to B\ne C$$
5		1hegrvtxdg1.x	$$⊢\phi \to E\in 𝒫V$$
6		1hegrvtxdg1.i	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,E⟩\right\}$$
7		1hegrvtxdg1.e	$$⊢\phi \to \left\{B,C\right\}\subseteq E$$
8		1hegrvtxdg1.v	$$⊢\phi \to \mathrm{Vtx}\left(G\right)=V$$
9		prid1g	$$⊢B\in V\to B\in \left\{B,C\right\}$$
10	2 9	syl	$$⊢\phi \to B\in \left\{B,C\right\}$$
11	7 10	sseldd	$$⊢\phi \to B\in E$$
12		prid2g	$$⊢C\in V\to C\in \left\{B,C\right\}$$
13	3 12	syl	$$⊢\phi \to C\in \left\{B,C\right\}$$
14	7 13	sseldd	$$⊢\phi \to C\in E$$
15	5 11 14 4	nehash2	$$⊢\phi \to 2\le \left|E\right|$$
16	6 8 1 2 5 11 15	1hevtxdg1	$$⊢\phi \to \mathrm{VtxDeg}\left(G\right)\left(B\right)=1$$