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	⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
Assertion	uspgrloopnb0	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
2	1	uspgrloopvtx	⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 )
3	2	3ad2ant1	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → ( Vtx ‘ 𝐺 ) = 𝑉 )
4		simp2	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → 𝐴 ∈ 𝑋 )
5		simp3	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ 𝑉 )
6	1	uspgrloopiedg	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
7	6	3adant3	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
8	3 4 5 7	1loopgrnb0	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = ∅ )