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