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 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 bitrdi 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