Metamath Proof Explorer

Theorem nbusgreledg

Description: A class/vertex is a neighbor of another class/vertex in a simple graph iff the vertices are endpoints of an edge. (Contributed by Alexander van der Vekens, 11-Oct-2017) (Revised by AV, 26-Oct-2020)

Ref Expression
Hypothesis nbusgreledg.e ⊢ E = Edg ⁡ G
Assertion nbusgreledg ⊢ G ∈ USGraph → N ∈ G NeighbVtx K ↔ N K ∈ E

Proof

Step Hyp Ref Expression
1 nbusgreledg.e ⊢ E = Edg ⁡ G
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 2 1 nbusgr ⊢ G ∈ USGraph → G NeighbVtx K = n ∈ Vtx ⁡ G | K n ∈ E
4 3 eleq2d ⊢ G ∈ USGraph → N ∈ G NeighbVtx K ↔ N ∈ n ∈ Vtx ⁡ G | K n ∈ E
5 1 2 usgrpredgv ⊢ G ∈ USGraph ∧ K N ∈ E → K ∈ Vtx ⁡ G ∧ N ∈ Vtx ⁡ G
6 5 simprd ⊢ G ∈ USGraph ∧ K N ∈ E → N ∈ Vtx ⁡ G
7 6 ex ⊢ G ∈ USGraph → K N ∈ E → N ∈ Vtx ⁡ G
8 7 pm4.71rd ⊢ G ∈ USGraph → K N ∈ E ↔ N ∈ Vtx ⁡ G ∧ K N ∈ E
9 prcom ⊢ N K = K N
10 9 eleq1i ⊢ N K ∈ E ↔ K N ∈ E
11 10 a1i ⊢ G ∈ USGraph → N K ∈ E ↔ K N ∈ E
12 preq2 ⊢ n = N → K n = K N
13 12 eleq1d ⊢ n = N → K n ∈ E ↔ K N ∈ E
14 13 elrab ⊢ N ∈ n ∈ Vtx ⁡ G | K n ∈ E ↔ N ∈ Vtx ⁡ G ∧ K N ∈ E
15 14 a1i ⊢ G ∈ USGraph → N ∈ n ∈ Vtx ⁡ G | K n ∈ E ↔ N ∈ Vtx ⁡ G ∧ K N ∈ E
16 8 11 15 3bitr4rd ⊢ G ∈ USGraph → N ∈ n ∈ Vtx ⁡ G | K n ∈ E ↔ N K ∈ E
17 4 16 bitrd ⊢ G ∈ USGraph → N ∈ G NeighbVtx K ↔ N K ∈ E