Metamath Proof Explorer

Theorem nbgrisvtx

Description: Every neighbor N of a vertex K is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020) (Revised by AV, 12-Feb-2022)

Ref Expression
Hypothesis nbgrisvtx.v ⊢ V = Vtx ⁡ G
Assertion nbgrisvtx ⊢ N ∈ G NeighbVtx K → N ∈ V

Proof

Step Hyp Ref Expression
1 nbgrisvtx.v ⊢ V = Vtx ⁡ G
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 1 2 nbgrel ⊢ N ∈ G NeighbVtx K ↔ N ∈ V ∧ K ∈ V ∧ N ≠ K ∧ ∃ e ∈ Edg ⁡ G K N ⊆ e
4 simp1l ⊢ N ∈ V ∧ K ∈ V ∧ N ≠ K ∧ ∃ e ∈ Edg ⁡ G K N ⊆ e → N ∈ V
5 3 4 sylbi ⊢ N ∈ G NeighbVtx K → N ∈ V