Metamath Proof Explorer


Theorem clnbgrssedg

Description: The vertices connected by an edge are a subset of the neigborhood of each of these vertices. (Contributed by AV, 26-May-2025) (Proof shortened by AV, 24-Aug-2025)

Ref Expression
Hypotheses clnbgrssedg.e 𝐸 = ( Edg ‘ 𝐺 )
clnbgrssedg.n 𝑁 = ( 𝐺 ClNeighbVtx 𝑋 )
Assertion clnbgrssedg ( ( 𝐺 ∈ UHGraph ∧ 𝐾𝐸𝑋𝐾 ) → 𝐾𝑁 )

Proof

Step Hyp Ref Expression
1 clnbgrssedg.e 𝐸 = ( Edg ‘ 𝐺 )
2 clnbgrssedg.n 𝑁 = ( 𝐺 ClNeighbVtx 𝑋 )
3 1 2 clnbgredg ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾𝐸𝑋𝐾𝑣𝐾 ) ) → 𝑣𝑁 )
4 3 3exp2 ( 𝐺 ∈ UHGraph → ( 𝐾𝐸 → ( 𝑋𝐾 → ( 𝑣𝐾𝑣𝑁 ) ) ) )
5 4 3imp ( ( 𝐺 ∈ UHGraph ∧ 𝐾𝐸𝑋𝐾 ) → ( 𝑣𝐾𝑣𝑁 ) )
6 5 ssrdv ( ( 𝐺 ∈ UHGraph ∧ 𝐾𝐸𝑋𝐾 ) → 𝐾𝑁 )