Metamath Proof Explorer

Theorem nbuhgr

Description: The set of neighbors of a vertex in a hypergraph. This version of nbgrval (with N being an arbitrary set instead of being a vertex) only holds for classes whose edges are subsets of the set of vertices (hypergraphs!). (Contributed by AV, 26-Oct-2020) (Proof shortened by AV, 15-Nov-2020)

Ref Expression
Hypotheses nbuhgr.v ⊢V=Vtx⁡G
nbuhgr.e ⊢E=Edg⁡G
Assertion nbuhgr ⊢G∈UHGraph∧N∈X→GNeighbVtxN=n∈V∖N|∃e∈ENn⊆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 a1d ⊢N∈V→G∈UHGraph∧N∈X→GNeighbVtxN=n∈V∖N|∃e∈ENn⊆e
5 df-nel ⊢N∉V↔¬N∈V
6 1 nbgrnvtx0 ⊢N∉V→GNeighbVtxN=∅
7 5 6 sylbir ⊢¬N∈V→GNeighbVtxN=∅
8 7 adantr ⊢¬N∈V∧G∈UHGraph∧N∈X→GNeighbVtxN=∅
9 simpl ⊢G∈UHGraph∧N∈X→G∈UHGraph
10 9 adantr ⊢G∈UHGraph∧N∈X∧n∈V∖N→G∈UHGraph
11 2 eleq2i ⊢e∈E↔e∈Edg⁡G
12 11 biimpi ⊢e∈E→e∈Edg⁡G
13 edguhgr ⊢G∈UHGraph∧e∈Edg⁡G→e∈𝒫Vtx⁡G
14 10 12 13 syl2an ⊢G∈UHGraph∧N∈X∧n∈V∖N∧e∈E→e∈𝒫Vtx⁡G
15 velpw ⊢e∈𝒫Vtx⁡G↔e⊆Vtx⁡G
16 1 eqcomi ⊢Vtx⁡G=V
17 16 sseq2i ⊢e⊆Vtx⁡G↔e⊆V
18 15 17 bitri ⊢e∈𝒫Vtx⁡G↔e⊆V
19 sstr ⊢Nn⊆e∧e⊆V→Nn⊆V
20 prssg ⊢N∈X∧n∈V→N∈V∧n∈V↔Nn⊆V
21 20 bicomd ⊢N∈X∧n∈V→Nn⊆V↔N∈V∧n∈V
22 21 elvd ⊢N∈X→Nn⊆V↔N∈V∧n∈V
23 simpl ⊢N∈V∧n∈V→N∈V
24 22 23 syl6bi ⊢N∈X→Nn⊆V→N∈V
25 19 24 syl5com ⊢Nn⊆e∧e⊆V→N∈X→N∈V
26 25 ex ⊢Nn⊆e→e⊆V→N∈X→N∈V
27 26 com13 ⊢N∈X→e⊆V→Nn⊆e→N∈V
28 27 ad3antlr ⊢G∈UHGraph∧N∈X∧n∈V∖N∧e∈E→e⊆V→Nn⊆e→N∈V
29 18 28 biimtrid ⊢G∈UHGraph∧N∈X∧n∈V∖N∧e∈E→e∈𝒫Vtx⁡G→Nn⊆e→N∈V
30 14 29 mpd ⊢G∈UHGraph∧N∈X∧n∈V∖N∧e∈E→Nn⊆e→N∈V
31 30 rexlimdva ⊢G∈UHGraph∧N∈X∧n∈V∖N→∃e∈ENn⊆e→N∈V
32 31 con3rr3 ⊢¬N∈V→G∈UHGraph∧N∈X∧n∈V∖N→¬∃e∈ENn⊆e
33 32 expdimp ⊢¬N∈V∧G∈UHGraph∧N∈X→n∈V∖N→¬∃e∈ENn⊆e
34 33 ralrimiv ⊢¬N∈V∧G∈UHGraph∧N∈X→∀n∈V∖N¬∃e∈ENn⊆e
35 rabeq0 ⊢n∈V∖N|∃e∈ENn⊆e=∅↔∀n∈V∖N¬∃e∈ENn⊆e
36 34 35 sylibr ⊢¬N∈V∧G∈UHGraph∧N∈X→n∈V∖N|∃e∈ENn⊆e=∅
37 8 36 eqtr4d ⊢¬N∈V∧G∈UHGraph∧N∈X→GNeighbVtxN=n∈V∖N|∃e∈ENn⊆e
38 37 ex ⊢¬N∈V→G∈UHGraph∧N∈X→GNeighbVtxN=n∈V∖N|∃e∈ENn⊆e
39 4 38 pm2.61i ⊢G∈UHGraph∧N∈X→GNeighbVtxN=n∈V∖N|∃e∈ENn⊆e