Database
GRAPH THEORY
Undirected graphs
Neighbors, complete graphs and universal vertices
Neighbors
nbupgrel
Next ⟩
nbumgrvtx
Metamath Proof Explorer
Ascii
Unicode
Theorem
nbupgrel
Description:
A neighbor of a vertex in a pseudograph.
(Contributed by
AV
, 5-Nov-2020)
Ref
Expression
Hypotheses
nbuhgr.v
⊢
V
=
Vtx
⁡
G
nbuhgr.e
⊢
E
=
Edg
⁡
G
Assertion
nbupgrel
⊢
G
∈
UPGraph
∧
K
∈
V
∧
N
∈
V
∧
N
≠
K
→
N
∈
G
NeighbVtx
K
↔
N
K
∈
E
Proof
Step
Hyp
Ref
Expression
1
nbuhgr.v
⊢
V
=
Vtx
⁡
G
2
nbuhgr.e
⊢
E
=
Edg
⁡
G
3
1
2
nbupgr
⊢
G
∈
UPGraph
∧
K
∈
V
→
G
NeighbVtx
K
=
n
∈
V
∖
K
|
K
n
∈
E
4
3
eleq2d
⊢
G
∈
UPGraph
∧
K
∈
V
→
N
∈
G
NeighbVtx
K
↔
N
∈
n
∈
V
∖
K
|
K
n
∈
E
5
preq2
⊢
n
=
N
→
K
n
=
K
N
6
5
eleq1d
⊢
n
=
N
→
K
n
∈
E
↔
K
N
∈
E
7
6
elrab
⊢
N
∈
n
∈
V
∖
K
|
K
n
∈
E
↔
N
∈
V
∖
K
∧
K
N
∈
E
8
4
7
syl6bb
⊢
G
∈
UPGraph
∧
K
∈
V
→
N
∈
G
NeighbVtx
K
↔
N
∈
V
∖
K
∧
K
N
∈
E
9
8
adantr
⊢
G
∈
UPGraph
∧
K
∈
V
∧
N
∈
V
∧
N
≠
K
→
N
∈
G
NeighbVtx
K
↔
N
∈
V
∖
K
∧
K
N
∈
E
10
eldifsn
⊢
N
∈
V
∖
K
↔
N
∈
V
∧
N
≠
K
11
10
biimpri
⊢
N
∈
V
∧
N
≠
K
→
N
∈
V
∖
K
12
11
adantl
⊢
G
∈
UPGraph
∧
K
∈
V
∧
N
∈
V
∧
N
≠
K
→
N
∈
V
∖
K
13
12
biantrurd
⊢
G
∈
UPGraph
∧
K
∈
V
∧
N
∈
V
∧
N
≠
K
→
K
N
∈
E
↔
N
∈
V
∖
K
∧
K
N
∈
E
14
prcom
⊢
K
N
=
N
K
15
14
eleq1i
⊢
K
N
∈
E
↔
N
K
∈
E
16
15
a1i
⊢
G
∈
UPGraph
∧
K
∈
V
∧
N
∈
V
∧
N
≠
K
→
K
N
∈
E
↔
N
K
∈
E
17
9
13
16
3bitr2d
⊢
G
∈
UPGraph
∧
K
∈
V
∧
N
∈
V
∧
N
≠
K
→
N
∈
G
NeighbVtx
K
↔
N
K
∈
E