Metamath Proof Explorer

Theorem vopnbgrelself

Description: A vertex N is a member of its semiopen neighborhood iff there is a loop joining the vertex with itself. (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 vopnbgrelself ⊢ N ∈ V → N ∈ U ↔ ∃ e ∈ E e = N

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 ibar ⊢ N ∈ V → ∃ e ∈ E N ≠ N ∧ N ∈ e ∧ N ∈ e ∨ N = N ∧ e = N ↔ N ∈ V ∧ ∃ e ∈ E N ≠ N ∧ N ∈ e ∧ N ∈ e ∨ N = N ∧ e = N
5 eqid ⊢ N = N
6 5 jctl ⊢ e = N → N = N ∧ e = N
7 6 olcd ⊢ e = N → N ≠ N ∧ N ∈ e ∧ N ∈ e ∨ N = N ∧ e = N
8 eqneqall ⊢ N = N → N ≠ N → N ∈ e ∧ N ∈ e → e = N
9 5 8 ax-mp ⊢ N ≠ N → N ∈ e ∧ N ∈ e → e = N
10 9 3impib ⊢ N ≠ N ∧ N ∈ e ∧ N ∈ e → e = N
11 simpr ⊢ N = N ∧ e = N → e = N
12 10 11 jaoi ⊢ N ≠ N ∧ N ∈ e ∧ N ∈ e ∨ N = N ∧ e = N → e = N
13 7 12 impbii ⊢ e = N ↔ N ≠ N ∧ N ∈ e ∧ N ∈ e ∨ N = N ∧ e = N
14 13 a1i ⊢ N ∈ V → e = N ↔ N ≠ N ∧ N ∈ e ∧ N ∈ e ∨ N = N ∧ e = N
15 14 rexbidv ⊢ N ∈ V → ∃ e ∈ E e = N ↔ ∃ e ∈ E N ≠ N ∧ N ∈ e ∧ N ∈ e ∨ N = N ∧ e = N
16 1 2 3 vopnbgrel ⊢ N ∈ V → N ∈ U ↔ N ∈ V ∧ ∃ e ∈ E N ≠ N ∧ N ∈ e ∧ N ∈ e ∨ N = N ∧ e = N
17 4 15 16 3bitr4rd ⊢ N ∈ V → N ∈ U ↔ ∃ e ∈ E e = N