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 𝑉 = ( Vtx ‘ 𝐺 )
Assertion nbgrisvtx ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) → 𝑁𝑉 )

Proof

Step Hyp Ref Expression
1 nbgrisvtx.v 𝑉 = ( Vtx ‘ 𝐺 )
2 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 nbgrel ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ ( ( 𝑁𝑉𝐾𝑉 ) ∧ 𝑁𝐾 ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ) )
4 simp1l ( ( ( 𝑁𝑉𝐾𝑉 ) ∧ 𝑁𝐾 ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ) → 𝑁𝑉 )
5 3 4 sylbi ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) → 𝑁𝑉 )