Metamath Proof Explorer

Theorem vopnbgrel

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

Ref Expression
Hypotheses dfvopnbgr2.v ⊢ V = Vtx ⁡ G
dfvopnbgr2.e ⊢ E = Edg ⁡ G
dfvopnbgr2.u ⊢ U = n ∈ V | n ∈ G NeighbVtx N ∨ ∃ e ∈ E N = n ∧ e = N
Assertion vopnbgrel ⊢ N ∈ V → X ∈ U ↔ X ∈ V ∧ ∃ e ∈ E X ≠ N ∧ N ∈ e ∧ X ∈ e ∨ X = N ∧ e = X

Proof

Step Hyp Ref Expression
1 dfvopnbgr2.v ⊢ V = Vtx ⁡ G
2 dfvopnbgr2.e ⊢ E = Edg ⁡ G
3 dfvopnbgr2.u ⊢ U = n ∈ V | n ∈ G NeighbVtx N ∨ ∃ e ∈ E N = n ∧ e = N
4 1 2 3 dfvopnbgr2 ⊢ N ∈ V → U = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n
5 4 eleq2d ⊢ N ∈ V → X ∈ U ↔ X ∈ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n
6 neeq1 ⊢ n = X → n ≠ N ↔ X ≠ N
7 eleq1 ⊢ n = X → n ∈ e ↔ X ∈ e
8 6 7 3anbi13d ⊢ n = X → n ≠ N ∧ N ∈ e ∧ n ∈ e ↔ X ≠ N ∧ N ∈ e ∧ X ∈ e
9 eqeq1 ⊢ n = X → n = N ↔ X = N
10 sneq ⊢ n = X → n = X
11 10 eqeq2d ⊢ n = X → e = n ↔ e = X
12 9 11 anbi12d ⊢ n = X → n = N ∧ e = n ↔ X = N ∧ e = X
13 8 12 orbi12d ⊢ n = X → n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ↔ X ≠ N ∧ N ∈ e ∧ X ∈ e ∨ X = N ∧ e = X
14 13 rexbidv ⊢ n = X → ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ↔ ∃ e ∈ E X ≠ N ∧ N ∈ e ∧ X ∈ e ∨ X = N ∧ e = X
15 14 elrab ⊢ X ∈ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ↔ X ∈ V ∧ ∃ e ∈ E X ≠ N ∧ N ∈ e ∧ X ∈ e ∨ X = N ∧ e = X
16 5 15 bitrdi ⊢ N ∈ V → X ∈ U ↔ X ∈ V ∧ ∃ e ∈ E X ≠ N ∧ N ∈ e ∧ X ∈ e ∨ X = N ∧ e = X