This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑋 ) )