This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion nbusgreledg ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 nbusgreledg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 2 1 nbusgr ⊢ ( 𝐺 ∈ USGraph → ( 𝐺 NeighbVtx 𝐾 ) = { 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } )
4 3 eleq2d ⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ 𝑁 ∈ { 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) )
5 1 2 usgrpredgv ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) → ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
6 5 simprd ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
7 6 ex ⊢ ( 𝐺 ∈ USGraph → ( { 𝐾 , 𝑁 } ∈ 𝐸 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
8 7 pm4.71rd ⊢ ( 𝐺 ∈ USGraph → ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) )
9 prcom ⊢ { 𝑁 , 𝐾 } = { 𝐾 , 𝑁 }
10 9 eleq1i ⊢ ( { 𝑁 , 𝐾 } ∈ 𝐸 ↔ { 𝐾 , 𝑁 } ∈ 𝐸 )
11 10 a1i ⊢ ( 𝐺 ∈ USGraph → ( { 𝑁 , 𝐾 } ∈ 𝐸 ↔ { 𝐾 , 𝑁 } ∈ 𝐸 ) )
12 preq2 ⊢ ( 𝑛 = 𝑁 → { 𝐾 , 𝑛 } = { 𝐾 , 𝑁 } )
13 12 eleq1d ⊢ ( 𝑛 = 𝑁 → ( { 𝐾 , 𝑛 } ∈ 𝐸 ↔ { 𝐾 , 𝑁 } ∈ 𝐸 ) )
14 13 elrab ⊢ ( 𝑁 ∈ { 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ↔ ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) )
15 14 a1i ⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ { 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ↔ ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) )
16 8 11 15 3bitr4rd ⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ { 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) )
17 4 16 bitrd ⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) )