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

Metamath Proof Explorer

Theorem 1hegrvtxdg1r

Description: The vertex degree of a graph with one hyperedge, 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, 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 1hegrvtxdg1r 
|- ( ph -> ( ( VtxDeg ` G ) ` C ) = 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 4 necomd 
 |-  ( ph -> C =/= B )
10 prcom 
 |-  { C , B } = { B , C }
11 10 7 eqsstrid 
 |-  ( ph -> { C , B } C_ E )
12 1 3 2 9 5 6 11 8 1hegrvtxdg1 
 |-  ( ph -> ( ( VtxDeg ` G ) ` C ) = 1 )