Metamath Proof Explorer

Theorem uhgrnbgr0nb

Description: A vertex which is not endpoint of an edge has no neighbor in a hypergraph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020)

Ref Expression
Assertion uhgrnbgr0nb ⊢G∈UHGraph∧∀e∈Edg⁡GN∉e→GNeighbVtxN=∅

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢Edg⁡G=Edg⁡G
3 1 2 nbuhgr ⊢G∈UHGraph∧N∈V→GNeighbVtxN=n∈Vtx⁡G∖N|∃e∈Edg⁡GNn⊆e
4 3 adantlr ⊢G∈UHGraph∧∀e∈Edg⁡GN∉e∧N∈V→GNeighbVtxN=n∈Vtx⁡G∖N|∃e∈Edg⁡GNn⊆e
5 df-nel ⊢N∉e↔¬N∈e
6 prssg ⊢N∈V∧n∈Vtx⁡G∖N→N∈e∧n∈e↔Nn⊆e
7 simpl ⊢N∈e∧n∈e→N∈e
8 6 7 syl6bir ⊢N∈V∧n∈Vtx⁡G∖N→Nn⊆e→N∈e
9 8 ad2antlr ⊢G∈UHGraph∧N∈V∧n∈Vtx⁡G∖N∧e∈Edg⁡G→Nn⊆e→N∈e
10 9 con3d ⊢G∈UHGraph∧N∈V∧n∈Vtx⁡G∖N∧e∈Edg⁡G→¬N∈e→¬Nn⊆e
11 5 10 biimtrid ⊢G∈UHGraph∧N∈V∧n∈Vtx⁡G∖N∧e∈Edg⁡G→N∉e→¬Nn⊆e
12 11 ralimdva ⊢G∈UHGraph∧N∈V∧n∈Vtx⁡G∖N→∀e∈Edg⁡GN∉e→∀e∈Edg⁡G¬Nn⊆e
13 12 imp ⊢G∈UHGraph∧N∈V∧n∈Vtx⁡G∖N∧∀e∈Edg⁡GN∉e→∀e∈Edg⁡G¬Nn⊆e
14 ralnex ⊢∀e∈Edg⁡G¬Nn⊆e↔¬∃e∈Edg⁡GNn⊆e
15 13 14 sylib ⊢G∈UHGraph∧N∈V∧n∈Vtx⁡G∖N∧∀e∈Edg⁡GN∉e→¬∃e∈Edg⁡GNn⊆e
16 15 expcom ⊢∀e∈Edg⁡GN∉e→G∈UHGraph∧N∈V∧n∈Vtx⁡G∖N→¬∃e∈Edg⁡GNn⊆e
17 16 expd ⊢∀e∈Edg⁡GN∉e→G∈UHGraph→N∈V∧n∈Vtx⁡G∖N→¬∃e∈Edg⁡GNn⊆e
18 17 impcom ⊢G∈UHGraph∧∀e∈Edg⁡GN∉e→N∈V∧n∈Vtx⁡G∖N→¬∃e∈Edg⁡GNn⊆e
19 18 expdimp ⊢G∈UHGraph∧∀e∈Edg⁡GN∉e∧N∈V→n∈Vtx⁡G∖N→¬∃e∈Edg⁡GNn⊆e
20 19 ralrimiv ⊢G∈UHGraph∧∀e∈Edg⁡GN∉e∧N∈V→∀n∈Vtx⁡G∖N¬∃e∈Edg⁡GNn⊆e
21 rabeq0 ⊢n∈Vtx⁡G∖N|∃e∈Edg⁡GNn⊆e=∅↔∀n∈Vtx⁡G∖N¬∃e∈Edg⁡GNn⊆e
22 20 21 sylibr ⊢G∈UHGraph∧∀e∈Edg⁡GN∉e∧N∈V→n∈Vtx⁡G∖N|∃e∈Edg⁡GNn⊆e=∅
23 4 22 eqtrd ⊢G∈UHGraph∧∀e∈Edg⁡GN∉e∧N∈V→GNeighbVtxN=∅
24 23 expcom ⊢N∈V→G∈UHGraph∧∀e∈Edg⁡GN∉e→GNeighbVtxN=∅
25 id ⊢¬N∈V→¬N∈V
26 25 intnand ⊢¬N∈V→¬G∈V∧N∈V
27 nbgrprc0 ⊢¬G∈V∧N∈V→GNeighbVtxN=∅
28 26 27 syl ⊢¬N∈V→GNeighbVtxN=∅
29 28 a1d ⊢¬N∈V→G∈UHGraph∧∀e∈Edg⁡GN∉e→GNeighbVtxN=∅
30 24 29 pm2.61i ⊢G∈UHGraph∧∀e∈Edg⁡GN∉e→GNeighbVtxN=∅