Theorem 1egrvtxdg1r

Description: The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given 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, 21-Feb-2021)

	Ref	Expression
Hypotheses	1egrvtxdg1.v	|- ( ph -> ( Vtx ` G ) = V )
	1egrvtxdg1.a	|- ( ph -> A e. X )
	1egrvtxdg1.b	|- ( ph -> B e. V )
	1egrvtxdg1.c	|- ( ph -> C e. V )
	1egrvtxdg1.n	|- ( ph -> B =/= C )
	1egrvtxdg1.i	|- ( ph -> ( iEdg ` G ) = { <. A , { B , C } >. } )
Assertion	1egrvtxdg1r	|- ( ph -> ( ( VtxDeg ` G ) ` C ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		1egrvtxdg1.v	|- ( ph -> ( Vtx ` G ) = V )
2		1egrvtxdg1.a	|- ( ph -> A e. X )
3		1egrvtxdg1.b	|- ( ph -> B e. V )
4		1egrvtxdg1.c	|- ( ph -> C e. V )
5		1egrvtxdg1.n	|- ( ph -> B =/= C )
6		1egrvtxdg1.i	|- ( ph -> ( iEdg ` G ) = { <. A , { B , C } >. } )
7	5	necomd	|- ( ph -> C =/= B )
8		prcom	|- { B , C } = { C , B }
9	8	a1i	|- ( ph -> { B , C } = { C , B } )
10	9	opeq2d	|- ( ph -> <. A , { B , C } >. = <. A , { C , B } >. )
11	10	sneqd	|- ( ph -> { <. A , { B , C } >. } = { <. A , { C , B } >. } )
12	6 11	eqtrd	|- ( ph -> ( iEdg ` G ) = { <. A , { C , B } >. } )
13	1 2 4 3 7 12	1egrvtxdg1	|- ( ph -> ( ( VtxDeg ` G ) ` C ) = 1 )