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 \in W \land A \in X \land N \in V) \to G NeighbVtx N = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	$⊢ G = ⟨V, \{⟨A, \{N\}⟩\}⟩$
2	1	uspgrloopvtx	$⊢ V \in W \to Vtx (G) = V$
3	2	3ad2ant1	$⊢ (V \in W \land A \in X \land N \in V) \to Vtx (G) = V$
4		simp2	$⊢ (V \in W \land A \in X \land N \in V) \to A \in X$
5		simp3	$⊢ (V \in W \land A \in X \land N \in V) \to N \in V$
6	1	uspgrloopiedg	$⊢ (V \in W \land A \in X) \to iEdg (G) = \{⟨A, \{N\}⟩\}$
7	6	3adant3	$⊢ (V \in W \land A \in X \land N \in V) \to iEdg (G) = \{⟨A, \{N\}⟩\}$
8	3 4 5 7	1loopgrnb0	$⊢ (V \in W \land A \in X \land N \in V) \to G NeighbVtx N = \emptyset$

Metamath Proof Explorer

Theorem uspgrloopnb0

Proof