Metamath Proof Explorer

Theorem nbupgr

Description: The set of neighbors of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020) (Proof shortened by AV, 30-Dec-2020)

Ref Expression
Hypotheses nbuhgr.v ⊢V=Vtx⁡G
nbuhgr.e ⊢E=Edg⁡G
Assertion nbupgr ⊢G∈UPGraph∧N∈V→GNeighbVtxN=n∈V∖N|Nn∈E

Proof

Step Hyp Ref Expression
1 nbuhgr.v ⊢V=Vtx⁡G
2 nbuhgr.e ⊢E=Edg⁡G
3 1 2 nbgrval ⊢N∈V→GNeighbVtxN=n∈V∖N|∃e∈ENn⊆e
4 3 adantl ⊢G∈UPGraph∧N∈V→GNeighbVtxN=n∈V∖N|∃e∈ENn⊆e
5 simp-4l ⊢G∈UPGraph∧N∈V∧n∈V∖N∧e∈E∧Nn⊆e→G∈UPGraph
6 simpr ⊢G∈UPGraph∧N∈V∧n∈V∖N∧e∈E→e∈E
7 6 adantr ⊢G∈UPGraph∧N∈V∧n∈V∖N∧e∈E∧Nn⊆e→e∈E
8 simpr ⊢G∈UPGraph∧N∈V∧n∈V∖N∧e∈E∧Nn⊆e→Nn⊆e
9 simpr ⊢G∈UPGraph∧N∈V→N∈V
10 9 adantr ⊢G∈UPGraph∧N∈V∧n∈V∖N→N∈V
11 vex ⊢n∈V
12 11 a1i ⊢G∈UPGraph∧N∈V∧n∈V∖N→n∈V
13 eldifsn ⊢n∈V∖N↔n∈V∧n≠N
14 simpr ⊢n∈V∧n≠N→n≠N
15 14 necomd ⊢n∈V∧n≠N→N≠n
16 13 15 sylbi ⊢n∈V∖N→N≠n
17 16 adantl ⊢G∈UPGraph∧N∈V∧n∈V∖N→N≠n
18 10 12 17 3jca ⊢G∈UPGraph∧N∈V∧n∈V∖N→N∈V∧n∈V∧N≠n
19 18 adantr ⊢G∈UPGraph∧N∈V∧n∈V∖N∧e∈E→N∈V∧n∈V∧N≠n
20 19 adantr ⊢G∈UPGraph∧N∈V∧n∈V∖N∧e∈E∧Nn⊆e→N∈V∧n∈V∧N≠n
21 1 2 upgredgpr ⊢G∈UPGraph∧e∈E∧Nn⊆e∧N∈V∧n∈V∧N≠n→Nn=e
22 5 7 8 20 21 syl31anc ⊢G∈UPGraph∧N∈V∧n∈V∖N∧e∈E∧Nn⊆e→Nn=e
23 22 ex ⊢G∈UPGraph∧N∈V∧n∈V∖N∧e∈E→Nn⊆e→Nn=e
24 eleq1 ⊢Nn=e→Nn∈E↔e∈E
25 24 biimprd ⊢Nn=e→e∈E→Nn∈E
26 23 6 25 syl6ci ⊢G∈UPGraph∧N∈V∧n∈V∖N∧e∈E→Nn⊆e→Nn∈E
27 26 rexlimdva ⊢G∈UPGraph∧N∈V∧n∈V∖N→∃e∈ENn⊆e→Nn∈E
28 simpr ⊢G∈UPGraph∧N∈V∧n∈V∖N∧Nn∈E→Nn∈E
29 sseq2 ⊢e=Nn→Nn⊆e↔Nn⊆Nn
30 29 adantl ⊢G∈UPGraph∧N∈V∧n∈V∖N∧Nn∈E∧e=Nn→Nn⊆e↔Nn⊆Nn
31 ssidd ⊢G∈UPGraph∧N∈V∧n∈V∖N∧Nn∈E→Nn⊆Nn
32 28 30 31 rspcedvd ⊢G∈UPGraph∧N∈V∧n∈V∖N∧Nn∈E→∃e∈ENn⊆e
33 32 ex ⊢G∈UPGraph∧N∈V∧n∈V∖N→Nn∈E→∃e∈ENn⊆e
34 27 33 impbid ⊢G∈UPGraph∧N∈V∧n∈V∖N→∃e∈ENn⊆e↔Nn∈E
35 34 rabbidva ⊢G∈UPGraph∧N∈V→n∈V∖N|∃e∈ENn⊆e=n∈V∖N|Nn∈E
36 4 35 eqtrd ⊢G∈UPGraph∧N∈V→GNeighbVtxN=n∈V∖N|Nn∈E