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	|- ( ph -> A e. X )
	1hegrvtxdg1.b	|- ( ph -> B e. V )
	1hegrvtxdg1.c	|- ( ph -> C e. V )
	1hegrvtxdg1.n	|- ( ph -> B =/= C )
	1hegrvtxdg1.x	|- ( ph -> E e. ~P V )
	1hegrvtxdg1.i	|- ( ph -> ( iEdg ` G ) = { <. A , E >. } )
	1hegrvtxdg1.e	|- ( ph -> { B , C } C_ E )
	1hegrvtxdg1.v	|- ( ph -> ( Vtx ` G ) = V )
Assertion	1hegrvtxdg1	|- ( ph -> ( ( VtxDeg ` G ) ` B ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		1hegrvtxdg1.a	|- ( ph -> A e. X )
2		1hegrvtxdg1.b	|- ( ph -> B e. V )
3		1hegrvtxdg1.c	|- ( ph -> C e. V )
4		1hegrvtxdg1.n	|- ( ph -> B =/= C )
5		1hegrvtxdg1.x	|- ( ph -> E e. ~P V )
6		1hegrvtxdg1.i	|- ( ph -> ( iEdg ` G ) = { <. A , E >. } )
7		1hegrvtxdg1.e	|- ( ph -> { B , C } C_ E )
8		1hegrvtxdg1.v	|- ( ph -> ( Vtx ` G ) = V )
9		prid1g	|- ( B e. V -> B e. { B , C } )
10	2 9	syl	|- ( ph -> B e. { B , C } )
11	7 10	sseldd	|- ( ph -> B e. E )
12		prid2g	|- ( C e. V -> C e. { B , C } )
13	3 12	syl	|- ( ph -> C e. { B , C } )
14	7 13	sseldd	|- ( ph -> C e. E )
15	5 11 14 4	nehash2	|- ( ph -> 2 <_ ( # ` E ) )
16	6 8 1 2 5 11 15	1hevtxdg1	|- ( ph -> ( ( VtxDeg ` G ) ` B ) = 1 )