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 ⊢ E = Edg ⁡ G
Assertion clnbupgreli ⊢ G ∈ UPGraph ∧ N ∈ G ClNeighbVtx K → N = K ∨ N K ∈ E

Proof

Step Hyp Ref Expression
1 clnbupgreli.e ⊢ E = Edg ⁡ G
2 simpr ⊢ G ∈ UPGraph ∧ N ∈ G ClNeighbVtx K → N ∈ G ClNeighbVtx K
3 simpl ⊢ G ∈ UPGraph ∧ N ∈ G ClNeighbVtx K → G ∈ UPGraph
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 4 clnbgrcl ⊢ N ∈ G ClNeighbVtx K → K ∈ Vtx ⁡ G
6 5 adantl ⊢ G ∈ UPGraph ∧ N ∈ G ClNeighbVtx K → K ∈ Vtx ⁡ G
7 4 clnbgrisvtx ⊢ N ∈ G ClNeighbVtx K → N ∈ Vtx ⁡ G
8 7 adantl ⊢ G ∈ UPGraph ∧ N ∈ G ClNeighbVtx K → N ∈ Vtx ⁡ G
9 4 1 clnbupgrel ⊢ G ∈ UPGraph ∧ K ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G → N ∈ G ClNeighbVtx K ↔ N = K ∨ N K ∈ E
10 3 6 8 9 syl3anc ⊢ G ∈ UPGraph ∧ N ∈ G ClNeighbVtx K → N ∈ G ClNeighbVtx K ↔ N = K ∨ N K ∈ E
11 2 10 mpbid ⊢ G ∈ UPGraph ∧ N ∈ G ClNeighbVtx K → N = K ∨ N K ∈ E