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	bilanri	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) ) → 𝑁 ∈ ( 𝑉 ∖ { 𝐾 } ) )
12	11	biantrurd	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) ) → ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ ( 𝑁 ∈ ( 𝑉 ∖ { 𝐾 } ) ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) )
13		prcom	⊢ { 𝐾 , 𝑁 } = { 𝑁 , 𝐾 }
14	13	eleq1i	⊢ ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ { 𝑁 , 𝐾 } ∈ 𝐸 )
15	14	a1i	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) ) → ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) )
16	9 12 15	3bitr2d	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾 ) ) → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) )