Metamath Proof Explorer

Theorem nbgr0vtx

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

Ref Expression
Assertion nbgr0vtx ⊢ Vtx ⁡ G = ∅ → G NeighbVtx K = ∅

Proof

Step Hyp Ref Expression
1 ral0 ⊢ ∀ n ∈ ∅ ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
2 difeq1 ⊢ Vtx ⁡ G = ∅ → Vtx ⁡ G ∖ K = ∅ ∖ K
3 0dif ⊢ ∅ ∖ K = ∅
4 2 3 eqtrdi ⊢ Vtx ⁡ G = ∅ → Vtx ⁡ G ∖ K = ∅
5 4 raleqdv ⊢ Vtx ⁡ G = ∅ → ∀ n ∈ Vtx ⁡ G ∖ K ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e ↔ ∀ n ∈ ∅ ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
6 1 5 mpbiri ⊢ Vtx ⁡ G = ∅ → ∀ n ∈ Vtx ⁡ G ∖ K ¬ ∃ e ∈ Edg ⁡ G K n ⊆ e
7 6 nbgr0vtxlem ⊢ Vtx ⁡ G = ∅ → G NeighbVtx K = ∅