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

Metamath Proof Explorer

Theorem uspgrloopnb0

Description: In a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop ), the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020) (Proof shortened by AV, 21-Feb-2021)

Ref Expression
Hypothesis uspgrloopvtx.g 
|- G = <. V , { <. A , { N } >. } >.
Assertion uspgrloopnb0 
|- ( ( V e. W /\ A e. X /\ N e. V ) -> ( G NeighbVtx N ) = (/) )

Proof

Step Hyp Ref Expression
1 uspgrloopvtx.g 
 |-  G = <. V , { <. A , { N } >. } >.
2 1 uspgrloopvtx 
 |-  ( V e. W -> ( Vtx ` G ) = V )
3 2 3ad2ant1 
 |-  ( ( V e. W /\ A e. X /\ N e. V ) -> ( Vtx ` G ) = V )
4 simp2 
 |-  ( ( V e. W /\ A e. X /\ N e. V ) -> A e. X )
5 simp3 
 |-  ( ( V e. W /\ A e. X /\ N e. V ) -> N e. V )
6 1 uspgrloopiedg 
 |-  ( ( V e. W /\ A e. X ) -> ( iEdg ` G ) = { <. A , { N } >. } )
7 6 3adant3 
 |-  ( ( V e. W /\ A e. X /\ N e. V ) -> ( iEdg ` G ) = { <. A , { N } >. } )
8 3 4 5 7 1loopgrnb0 
 |-  ( ( V e. W /\ A e. X /\ N e. V ) -> ( G NeighbVtx N ) = (/) )