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 → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ E N n ⊆ e

Proof

Step Hyp Ref Expression
1 nbuhgr.v ⊢ V = Vtx ⁡ G
2 nbuhgr.e ⊢ E = Edg ⁡ G
3 1 2 nbgrval ⊢ N ∈ V → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ E N n ⊆ e
4 3 a1d ⊢ N ∈ V → G ∈ UHGraph ∧ N ∈ X → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ E N n ⊆ e
5 df-nel ⊢ N ∉ V ↔ ¬ N ∈ V
6 1 nbgrnvtx0 ⊢ N ∉ V → G NeighbVtx N = ∅
7 5 6 sylbir ⊢ ¬ N ∈ V → G NeighbVtx N = ∅
8 7 adantr ⊢ ¬ N ∈ V ∧ G ∈ UHGraph ∧ N ∈ X → G NeighbVtx N = ∅
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 ⊢ N n ⊆ e ∧ e ⊆ V → N n ⊆ V
20 prssg ⊢ N ∈ X ∧ n ∈ V → N ∈ V ∧ n ∈ V ↔ N n ⊆ V
21 20 bicomd ⊢ N ∈ X ∧ n ∈ V → N n ⊆ V ↔ N ∈ V ∧ n ∈ V
22 21 elvd ⊢ N ∈ X → N n ⊆ V ↔ N ∈ V ∧ n ∈ V
23 simpl ⊢ N ∈ V ∧ n ∈ V → N ∈ V
24 22 23 syl6bi ⊢ N ∈ X → N n ⊆ V → N ∈ V
25 19 24 syl5com ⊢ N n ⊆ e ∧ e ⊆ V → N ∈ X → N ∈ V
26 25 ex ⊢ N n ⊆ e → e ⊆ V → N ∈ X → N ∈ V
27 26 com13 ⊢ N ∈ X → e ⊆ V → N n ⊆ e → N ∈ V
28 27 ad3antlr ⊢ G ∈ UHGraph ∧ N ∈ X ∧ n ∈ V ∖ N ∧ e ∈ E → e ⊆ V → N n ⊆ e → N ∈ V
29 18 28 syl5bi ⊢ G ∈ UHGraph ∧ N ∈ X ∧ n ∈ V ∖ N ∧ e ∈ E → e ∈ 𝒫 Vtx ⁡ G → N n ⊆ e → N ∈ V
30 14 29 mpd ⊢ G ∈ UHGraph ∧ N ∈ X ∧ n ∈ V ∖ N ∧ e ∈ E → N n ⊆ e → N ∈ V
31 30 rexlimdva ⊢ G ∈ UHGraph ∧ N ∈ X ∧ n ∈ V ∖ N → ∃ e ∈ E N n ⊆ e → N ∈ V
32 31 con3rr3 ⊢ ¬ N ∈ V → G ∈ UHGraph ∧ N ∈ X ∧ n ∈ V ∖ N → ¬ ∃ e ∈ E N n ⊆ e
33 32 expdimp ⊢ ¬ N ∈ V ∧ G ∈ UHGraph ∧ N ∈ X → n ∈ V ∖ N → ¬ ∃ e ∈ E N n ⊆ e
34 33 ralrimiv ⊢ ¬ N ∈ V ∧ G ∈ UHGraph ∧ N ∈ X → ∀ n ∈ V ∖ N ¬ ∃ e ∈ E N n ⊆ e
35 rabeq0 ⊢ n ∈ V ∖ N | ∃ e ∈ E N n ⊆ e = ∅ ↔ ∀ n ∈ V ∖ N ¬ ∃ e ∈ E N n ⊆ e
36 34 35 sylibr ⊢ ¬ N ∈ V ∧ G ∈ UHGraph ∧ N ∈ X → n ∈ V ∖ N | ∃ e ∈ E N n ⊆ e = ∅
37 8 36 eqtr4d ⊢ ¬ N ∈ V ∧ G ∈ UHGraph ∧ N ∈ X → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ E N n ⊆ e
38 37 ex ⊢ ¬ N ∈ V → G ∈ UHGraph ∧ N ∈ X → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ E N n ⊆ e
39 4 38 pm2.61i ⊢ G ∈ UHGraph ∧ N ∈ X → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ E N n ⊆ e