Metamath Proof Explorer

Theorem clnbgrel

Description: Characterization of a member N of the closed neighborhood of a vertex X in a graph G . (Contributed by AV, 9-May-2025)

Ref Expression
Hypotheses clnbgrel.v ⊢ V = Vtx ⁡ G
clnbgrel.e ⊢ E = Edg ⁡ G
Assertion clnbgrel ⊢ N ∈ G ClNeighbVtx X ↔ N ∈ V ∧ X ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e

Proof

Step Hyp Ref Expression
1 clnbgrel.v ⊢ V = Vtx ⁡ G
2 clnbgrel.e ⊢ E = Edg ⁡ G
3 1 clnbgrcl ⊢ N ∈ G ClNeighbVtx X → X ∈ V
4 3 pm4.71ri ⊢ N ∈ G ClNeighbVtx X ↔ X ∈ V ∧ N ∈ G ClNeighbVtx X
5 1 2 clnbgrval ⊢ X ∈ V → G ClNeighbVtx X = X ∪ n ∈ V | ∃ e ∈ E X n ⊆ e
6 5 eleq2d ⊢ X ∈ V → N ∈ G ClNeighbVtx X ↔ N ∈ X ∪ n ∈ V | ∃ e ∈ E X n ⊆ e
7 elun ⊢ N ∈ X ∪ n ∈ V | ∃ e ∈ E X n ⊆ e ↔ N ∈ X ∨ N ∈ n ∈ V | ∃ e ∈ E X n ⊆ e
8 elsn2g ⊢ X ∈ V → N ∈ X ↔ N = X
9 preq2 ⊢ n = N → X n = X N
10 9 sseq1d ⊢ n = N → X n ⊆ e ↔ X N ⊆ e
11 10 rexbidv ⊢ n = N → ∃ e ∈ E X n ⊆ e ↔ ∃ e ∈ E X N ⊆ e
12 11 elrab ⊢ N ∈ n ∈ V | ∃ e ∈ E X n ⊆ e ↔ N ∈ V ∧ ∃ e ∈ E X N ⊆ e
13 12 a1i ⊢ X ∈ V → N ∈ n ∈ V | ∃ e ∈ E X n ⊆ e ↔ N ∈ V ∧ ∃ e ∈ E X N ⊆ e
14 8 13 orbi12d ⊢ X ∈ V → N ∈ X ∨ N ∈ n ∈ V | ∃ e ∈ E X n ⊆ e ↔ N = X ∨ N ∈ V ∧ ∃ e ∈ E X N ⊆ e
15 7 14 bitrid ⊢ X ∈ V → N ∈ X ∪ n ∈ V | ∃ e ∈ E X n ⊆ e ↔ N = X ∨ N ∈ V ∧ ∃ e ∈ E X N ⊆ e
16 eleq1 ⊢ N = X → N ∈ V ↔ X ∈ V
17 16 biimparc ⊢ X ∈ V ∧ N = X → N ∈ V
18 orc ⊢ N = X → N = X ∨ ∃ e ∈ E X N ⊆ e
19 18 adantl ⊢ X ∈ V ∧ N = X → N = X ∨ ∃ e ∈ E X N ⊆ e
20 17 19 jca ⊢ X ∈ V ∧ N = X → N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
21 20 ex ⊢ X ∈ V → N = X → N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
22 olc ⊢ ∃ e ∈ E X N ⊆ e → N = X ∨ ∃ e ∈ E X N ⊆ e
23 22 anim2i ⊢ N ∈ V ∧ ∃ e ∈ E X N ⊆ e → N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
24 23 a1i ⊢ X ∈ V → N ∈ V ∧ ∃ e ∈ E X N ⊆ e → N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
25 21 24 jaod ⊢ X ∈ V → N = X ∨ N ∈ V ∧ ∃ e ∈ E X N ⊆ e → N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
26 orc ⊢ N = X → N = X ∨ N ∈ V ∧ ∃ e ∈ E X N ⊆ e
27 26 a1i ⊢ X ∈ V ∧ N ∈ V → N = X → N = X ∨ N ∈ V ∧ ∃ e ∈ E X N ⊆ e
28 olc ⊢ N ∈ V ∧ ∃ e ∈ E X N ⊆ e → N = X ∨ N ∈ V ∧ ∃ e ∈ E X N ⊆ e
29 28 ex ⊢ N ∈ V → ∃ e ∈ E X N ⊆ e → N = X ∨ N ∈ V ∧ ∃ e ∈ E X N ⊆ e
30 29 adantl ⊢ X ∈ V ∧ N ∈ V → ∃ e ∈ E X N ⊆ e → N = X ∨ N ∈ V ∧ ∃ e ∈ E X N ⊆ e
31 27 30 jaod ⊢ X ∈ V ∧ N ∈ V → N = X ∨ ∃ e ∈ E X N ⊆ e → N = X ∨ N ∈ V ∧ ∃ e ∈ E X N ⊆ e
32 31 expimpd ⊢ X ∈ V → N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e → N = X ∨ N ∈ V ∧ ∃ e ∈ E X N ⊆ e
33 25 32 impbid ⊢ X ∈ V → N = X ∨ N ∈ V ∧ ∃ e ∈ E X N ⊆ e ↔ N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
34 6 15 33 3bitrd ⊢ X ∈ V → N ∈ G ClNeighbVtx X ↔ N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
35 34 pm5.32i ⊢ X ∈ V ∧ N ∈ G ClNeighbVtx X ↔ X ∈ V ∧ N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
36 anass ⊢ X ∈ V ∧ N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e ↔ X ∈ V ∧ N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
37 36 bicomi ⊢ X ∈ V ∧ N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e ↔ X ∈ V ∧ N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
38 ancom ⊢ X ∈ V ∧ N ∈ V ↔ N ∈ V ∧ X ∈ V
39 37 38 bianbi ⊢ X ∈ V ∧ N ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e ↔ N ∈ V ∧ X ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e
40 4 35 39 3bitri ⊢ N ∈ G ClNeighbVtx X ↔ N ∈ V ∧ X ∈ V ∧ N = X ∨ ∃ e ∈ E X N ⊆ e