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

Metamath Proof Explorer

Theorem clnbupgreli

Description: A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 28-Dec-2025)

Ref Expression
Hypothesis clnbupgreli.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion clnbupgreli ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ) → ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 clnbupgreli.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 simpr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ) → 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) )
3 simpl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ) → 𝐺 ∈ UPGraph )
4 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 4 clnbgrcl ⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) → 𝐾 ∈ ( Vtx ‘ 𝐺 ) )
6 5 adantl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ) → 𝐾 ∈ ( Vtx ‘ 𝐺 ) )
7 4 clnbgrisvtx ⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
8 7 adantl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
9 4 1 clnbupgrel ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) )
10 3 6 8 9 syl3anc ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ) → ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) )
11 2 10 mpbid ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ) → ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) )