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 ⁡ G N ∉ e → G NeighbVtx N = ∅

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