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 ) = (/) )