Metamath Proof Explorer

Theorem nbgr1vtx

Description: In a graph with one vertex, all neighborhoods are empty. (Contributed by AV, 15-Nov-2020)

Ref Expression
Assertion nbgr1vtx ⊢Vtx⁡G=1→GNeighbVtxK=∅

Proof

Step Hyp Ref Expression
1 fvex ⊢Vtx⁡G∈V
2 hash1snb ⊢Vtx⁡G∈V→Vtx⁡G=1↔∃vVtx⁡G=v
3 1 2 ax-mp ⊢Vtx⁡G=1↔∃vVtx⁡G=v
4 ral0 ⊢∀n∈∅¬∃e∈Edg⁡GKn⊆e
5 eleq2 ⊢Vtx⁡G=v→K∈Vtx⁡G↔K∈v
6 simpr ⊢K=v∧Vtx⁡G=v→Vtx⁡G=v
7 sneq ⊢K=v→K=v
8 7 adantr ⊢K=v∧Vtx⁡G=v→K=v
9 6 8 difeq12d ⊢K=v∧Vtx⁡G=v→Vtx⁡G∖K=v∖v
10 difid ⊢v∖v=∅
11 9 10 eqtrdi ⊢K=v∧Vtx⁡G=v→Vtx⁡G∖K=∅
12 11 ex ⊢K=v→Vtx⁡G=v→Vtx⁡G∖K=∅
13 elsni ⊢K∈v→K=v
14 12 13 syl11 ⊢Vtx⁡G=v→K∈v→Vtx⁡G∖K=∅
15 5 14 sylbid ⊢Vtx⁡G=v→K∈Vtx⁡G→Vtx⁡G∖K=∅
16 15 imp ⊢Vtx⁡G=v∧K∈Vtx⁡G→Vtx⁡G∖K=∅
17 16 raleqdv ⊢Vtx⁡G=v∧K∈Vtx⁡G→∀n∈Vtx⁡G∖K¬∃e∈Edg⁡GKn⊆e↔∀n∈∅¬∃e∈Edg⁡GKn⊆e
18 4 17 mpbiri ⊢Vtx⁡G=v∧K∈Vtx⁡G→∀n∈Vtx⁡G∖K¬∃e∈Edg⁡GKn⊆e
19 18 ex ⊢Vtx⁡G=v→K∈Vtx⁡G→∀n∈Vtx⁡G∖K¬∃e∈Edg⁡GKn⊆e
20 19 exlimiv ⊢∃vVtx⁡G=v→K∈Vtx⁡G→∀n∈Vtx⁡G∖K¬∃e∈Edg⁡GKn⊆e
21 3 20 sylbi ⊢Vtx⁡G=1→K∈Vtx⁡G→∀n∈Vtx⁡G∖K¬∃e∈Edg⁡GKn⊆e
22 21 impcom ⊢K∈Vtx⁡G∧Vtx⁡G=1→∀n∈Vtx⁡G∖K¬∃e∈Edg⁡GKn⊆e
23 22 nbgr0vtxlem ⊢K∈Vtx⁡G∧Vtx⁡G=1→GNeighbVtxK=∅
24 23 ex ⊢K∈Vtx⁡G→Vtx⁡G=1→GNeighbVtxK=∅
25 df-nel ⊢K∉Vtx⁡G↔¬K∈Vtx⁡G
26 eqid ⊢Vtx⁡G=Vtx⁡G
27 26 nbgrnvtx0 ⊢K∉Vtx⁡G→GNeighbVtxK=∅
28 25 27 sylbir ⊢¬K∈Vtx⁡G→GNeighbVtxK=∅
29 28 a1d ⊢¬K∈Vtx⁡G→Vtx⁡G=1→GNeighbVtxK=∅
30 24 29 pm2.61i ⊢Vtx⁡G=1→GNeighbVtxK=∅