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

Metamath Proof Explorer

Theorem nbupgrel

Description: A neighbor of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020)

Ref Expression
Hypotheses nbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion nbupgrel ( ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) ) → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 nbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 nbupgr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝐾 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝐾 } ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } )
4 3 eleq2d ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ 𝑁 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝐾 } ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) )
5 preq2 ⊢ ( 𝑛 = 𝑁 → { 𝐾 , 𝑛 } = { 𝐾 , 𝑁 } )
6 5 eleq1d ⊢ ( 𝑛 = 𝑁 → ( { 𝐾 , 𝑛 } ∈ 𝐸 ↔ { 𝐾 , 𝑁 } ∈ 𝐸 ) )
7 6 elrab ⊢ ( 𝑁 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝐾 } ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ↔ ( 𝑁 ∈ ( 𝑉 ∖ { 𝐾 } ) ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) )
8 4 7 bitrdi ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ ( 𝑁 ∈ ( 𝑉 ∖ { 𝐾 } ) ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) )
9 8 adantr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) ) → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ ( 𝑁 ∈ ( 𝑉 ∖ { 𝐾 } ) ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) )
10 eldifsn ⊢ ( 𝑁 ∈ ( 𝑉 ∖ { 𝐾 } ) ↔ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) )
11 10 biimpri ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) → 𝑁 ∈ ( 𝑉 ∖ { 𝐾 } ) )
12 11 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) ) → 𝑁 ∈ ( 𝑉 ∖ { 𝐾 } ) )
13 12 biantrurd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) ) → ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ ( 𝑁 ∈ ( 𝑉 ∖ { 𝐾 } ) ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) )
14 prcom ⊢ { 𝐾 , 𝑁 } = { 𝑁 , 𝐾 }
15 14 eleq1i ⊢ ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ { 𝑁 , 𝐾 } ∈ 𝐸 )
16 15 a1i ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) ) → ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) )
17 9 13 16 3bitr2d ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) ) → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) )