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 𝐾 ) ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) )