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∈GNeighbVtxK↔NK∈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→GNeighbVtxK=n∈V∖K|Kn∈E
4 3 eleq2d ⊢G∈UPGraph∧K∈V→N∈GNeighbVtxK↔N∈n∈V∖K|Kn∈E
5 preq2 ⊢n=N→Kn=KN
6 5 eleq1d ⊢n=N→Kn∈E↔KN∈E
7 6 elrab ⊢N∈n∈V∖K|Kn∈E↔N∈V∖K∧KN∈E
8 4 7 bitrdi ⊢G∈UPGraph∧K∈V→N∈GNeighbVtxK↔N∈V∖K∧KN∈E
9 8 adantr ⊢G∈UPGraph∧K∈V∧N∈V∧N≠K→N∈GNeighbVtxK↔N∈V∖K∧KN∈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→KN∈E↔N∈V∖K∧KN∈E
14 prcom ⊢KN=NK
15 14 eleq1i ⊢KN∈E↔NK∈E
16 15 a1i ⊢G∈UPGraph∧K∈V∧N∈V∧N≠K→KN∈E↔NK∈E
17 9 13 16 3bitr2d ⊢G∈UPGraph∧K∈V∧N∈V∧N≠K→N∈GNeighbVtxK↔NK∈E