Metamath Proof Explorer

Theorem clnbupgr

Description: The closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025)

Ref Expression
Hypotheses clnbuhgr.v ⊢ V = Vtx ⁡ G
clnbuhgr.e ⊢ E = Edg ⁡ G
Assertion clnbupgr ⊢ G ∈ UPGraph ∧ N ∈ V → G ClNeighbVtx N = N ∪ n ∈ V | N n ∈ E

Proof

Step Hyp Ref Expression
1 clnbuhgr.v ⊢ V = Vtx ⁡ G
2 clnbuhgr.e ⊢ E = Edg ⁡ G
3 1 dfclnbgr4 ⊢ N ∈ V → G ClNeighbVtx N = N ∪ G NeighbVtx N
4 3 adantl ⊢ G ∈ UPGraph ∧ N ∈ V → G ClNeighbVtx N = N ∪ G NeighbVtx N
5 1 2 nbupgr ⊢ G ∈ UPGraph ∧ N ∈ V → G NeighbVtx N = n ∈ V ∖ N | N n ∈ E
6 5 uneq2d ⊢ G ∈ UPGraph ∧ N ∈ V → N ∪ G NeighbVtx N = N ∪ n ∈ V ∖ N | N n ∈ E
7 rabdif ⊢ n ∈ V | N n ∈ E ∖ N = n ∈ V ∖ N | N n ∈ E
8 7 eqcomi ⊢ n ∈ V ∖ N | N n ∈ E = n ∈ V | N n ∈ E ∖ N
9 8 uneq2i ⊢ N ∪ n ∈ V ∖ N | N n ∈ E = N ∪ n ∈ V | N n ∈ E ∖ N
10 undif2 ⊢ N ∪ n ∈ V | N n ∈ E ∖ N = N ∪ n ∈ V | N n ∈ E
11 9 10 eqtri ⊢ N ∪ n ∈ V ∖ N | N n ∈ E = N ∪ n ∈ V | N n ∈ E
12 11 a1i ⊢ G ∈ UPGraph ∧ N ∈ V → N ∪ n ∈ V ∖ N | N n ∈ E = N ∪ n ∈ V | N n ∈ E
13 4 6 12 3eqtrd ⊢ G ∈ UPGraph ∧ N ∈ V → G ClNeighbVtx N = N ∪ n ∈ V | N n ∈ E