Metamath Proof Explorer

Theorem clnbupgrel

Description: A member of 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 clnbupgrel ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V → N ∈ G ClNeighbVtx K ↔ N = K ∨ N K ∈ E

Proof

Step Hyp Ref Expression
1 clnbuhgr.v ⊢ V = Vtx ⁡ G
2 clnbuhgr.e ⊢ E = Edg ⁡ G
3 1 2 clnbupgr ⊢ G ∈ UPGraph ∧ K ∈ V → G ClNeighbVtx K = K ∪ n ∈ V | K n ∈ E
4 3 eleq2d ⊢ G ∈ UPGraph ∧ K ∈ V → N ∈ G ClNeighbVtx K ↔ N ∈ K ∪ n ∈ V | K n ∈ E
5 4 3adant3 ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V → N ∈ G ClNeighbVtx K ↔ N ∈ K ∪ n ∈ V | K n ∈ E
6 elun ⊢ N ∈ K ∪ n ∈ V | K n ∈ E ↔ N ∈ K ∨ N ∈ n ∈ V | K n ∈ E
7 preq2 ⊢ n = N → K n = K N
8 7 eleq1d ⊢ n = N → K n ∈ E ↔ K N ∈ E
9 8 elrab ⊢ N ∈ n ∈ V | K n ∈ E ↔ N ∈ V ∧ K N ∈ E
10 9 orbi2i ⊢ N ∈ K ∨ N ∈ n ∈ V | K n ∈ E ↔ N ∈ K ∨ N ∈ V ∧ K N ∈ E
11 6 10 bitri ⊢ N ∈ K ∪ n ∈ V | K n ∈ E ↔ N ∈ K ∨ N ∈ V ∧ K N ∈ E
12 elsng ⊢ N ∈ V → N ∈ K ↔ N = K
13 12 3ad2ant3 ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V → N ∈ K ↔ N = K
14 13 orbi1d ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V → N ∈ K ∨ N ∈ V ∧ K N ∈ E ↔ N = K ∨ N ∈ V ∧ K N ∈ E
15 11 14 bitrid ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V → N ∈ K ∪ n ∈ V | K n ∈ E ↔ N = K ∨ N ∈ V ∧ K N ∈ E
16 ibar ⊢ N ∈ V → K N ∈ E ↔ N ∈ V ∧ K N ∈ E
17 prcom ⊢ K N = N K
18 17 eleq1i ⊢ K N ∈ E ↔ N K ∈ E
19 16 18 bitr3di ⊢ N ∈ V → N ∈ V ∧ K N ∈ E ↔ N K ∈ E
20 19 orbi2d ⊢ N ∈ V → N = K ∨ N ∈ V ∧ K N ∈ E ↔ N = K ∨ N K ∈ E
21 20 3ad2ant3 ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V → N = K ∨ N ∈ V ∧ K N ∈ E ↔ N = K ∨ N K ∈ E
22 5 15 21 3bitrd ⊢ G ∈ UPGraph ∧ K ∈ V ∧ N ∈ V → N ∈ G ClNeighbVtx K ↔ N = K ∨ N K ∈ E