Metamath Proof Explorer


Theorem predgclnbgrel

Description: If a (not necessarily proper) unordered pair containing a vertex is an edge, the other vertex is in the closed neighborhood of the first vertex. (Contributed by AV, 23-Aug-2025)

Ref Expression
Hypotheses predgclnbgrel.v 𝑉 = ( Vtx ‘ 𝐺 )
predgclnbgrel.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion predgclnbgrel ( ( 𝑁𝑉𝑋𝑉 ∧ { 𝑋 , 𝑁 } ∈ 𝐸 ) → 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) )

Proof

Step Hyp Ref Expression
1 predgclnbgrel.v 𝑉 = ( Vtx ‘ 𝐺 )
2 predgclnbgrel.e 𝐸 = ( Edg ‘ 𝐺 )
3 3simpa ( ( 𝑁𝑉𝑋𝑉 ∧ { 𝑋 , 𝑁 } ∈ 𝐸 ) → ( 𝑁𝑉𝑋𝑉 ) )
4 simp3 ( ( 𝑁𝑉𝑋𝑉 ∧ { 𝑋 , 𝑁 } ∈ 𝐸 ) → { 𝑋 , 𝑁 } ∈ 𝐸 )
5 sseq2 ( 𝑒 = { 𝑋 , 𝑁 } → ( { 𝑋 , 𝑁 } ⊆ 𝑒 ↔ { 𝑋 , 𝑁 } ⊆ { 𝑋 , 𝑁 } ) )
6 5 adantl ( ( ( 𝑁𝑉𝑋𝑉 ∧ { 𝑋 , 𝑁 } ∈ 𝐸 ) ∧ 𝑒 = { 𝑋 , 𝑁 } ) → ( { 𝑋 , 𝑁 } ⊆ 𝑒 ↔ { 𝑋 , 𝑁 } ⊆ { 𝑋 , 𝑁 } ) )
7 ssidd ( ( 𝑁𝑉𝑋𝑉 ∧ { 𝑋 , 𝑁 } ∈ 𝐸 ) → { 𝑋 , 𝑁 } ⊆ { 𝑋 , 𝑁 } )
8 4 6 7 rspcedvd ( ( 𝑁𝑉𝑋𝑉 ∧ { 𝑋 , 𝑁 } ∈ 𝐸 ) → ∃ 𝑒𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 )
9 8 olcd ( ( 𝑁𝑉𝑋𝑉 ∧ { 𝑋 , 𝑁 } ∈ 𝐸 ) → ( 𝑁 = 𝑋 ∨ ∃ 𝑒𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
10 1 2 clnbgrel ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ↔ ( ( 𝑁𝑉𝑋𝑉 ) ∧ ( 𝑁 = 𝑋 ∨ ∃ 𝑒𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
11 3 9 10 sylanbrc ( ( 𝑁𝑉𝑋𝑉 ∧ { 𝑋 , 𝑁 } ∈ 𝐸 ) → 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) )