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 → G NeighbVtx K = ∅

Proof

Step Hyp Ref Expression
1 fvex ⊢ Vtx ⁡ G ∈ V
2 hash1snb ⊢ Vtx ⁡ G ∈ V → Vtx ⁡ G = 1 ↔ ∃ v Vtx ⁡ G = v
3 1 2 ax-mp ⊢ Vtx ⁡ G = 1 ↔ ∃ v Vtx ⁡ G = v
4 ral0 ⊢ ∀ n ∈ ∅ ¬ ∃ e ∈ Edg ⁡ G K n ⊆ 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 ⁡ G K n ⊆ e ↔ ∀ n ∈ ∅ ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
18 4 17 mpbiri ⊢ Vtx ⁡ G = v ∧ K ∈ Vtx ⁡ G → ∀ n ∈ Vtx ⁡ G ∖ K ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
19 18 ex ⊢ Vtx ⁡ G = v → K ∈ Vtx ⁡ G → ∀ n ∈ Vtx ⁡ G ∖ K ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
20 19 exlimiv ⊢ ∃ v Vtx ⁡ G = v → K ∈ Vtx ⁡ G → ∀ n ∈ Vtx ⁡ G ∖ K ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
21 3 20 sylbi ⊢ Vtx ⁡ G = 1 → K ∈ Vtx ⁡ G → ∀ n ∈ Vtx ⁡ G ∖ K ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
22 21 impcom ⊢ K ∈ Vtx ⁡ G ∧ Vtx ⁡ G = 1 → ∀ n ∈ Vtx ⁡ G ∖ K ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
23 22 nbgr0edglem ⊢ K ∈ Vtx ⁡ G ∧ Vtx ⁡ G = 1 → G NeighbVtx K = ∅
24 23 ex ⊢ K ∈ Vtx ⁡ G → Vtx ⁡ G = 1 → G NeighbVtx K = ∅
25 df-nel ⊢ K ∉ Vtx ⁡ G ↔ ¬ K ∈ Vtx ⁡ G
26 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
27 26 nbgrnvtx0 ⊢ K ∉ Vtx ⁡ G → G NeighbVtx K = ∅
28 25 27 sylbir ⊢ ¬ K ∈ Vtx ⁡ G → G NeighbVtx K = ∅
29 28 a1d ⊢ ¬ K ∈ Vtx ⁡ G → Vtx ⁡ G = 1 → G NeighbVtx K = ∅
30 24 29 pm2.61i ⊢ Vtx ⁡ G = 1 → G NeighbVtx K = ∅