Metamath Proof Explorer

Theorem nbgr0vtxlem

Description: Lemma for nbgr0vtx and nbgr0edg . (Contributed by AV, 15-Nov-2020)

Ref Expression
Hypothesis nbgr0vtxlem.v ⊢φ→∀n∈Vtx⁡G∖K¬∃e∈Edg⁡GKn⊆e
Assertion nbgr0vtxlem ⊢φ→GNeighbVtxK=∅

Proof

Step Hyp Ref Expression
1 nbgr0vtxlem.v ⊢φ→∀n∈Vtx⁡G∖K¬∃e∈Edg⁡GKn⊆e
2 eqid ⊢Vtx⁡G=Vtx⁡G
3 eqid ⊢Edg⁡G=Edg⁡G
4 2 3 nbgrval ⊢K∈Vtx⁡G→GNeighbVtxK=n∈Vtx⁡G∖K|∃e∈Edg⁡GKn⊆e
5 4 ad2antrl ⊢G∈V∧K∈V∧K∈Vtx⁡G∧φ→GNeighbVtxK=n∈Vtx⁡G∖K|∃e∈Edg⁡GKn⊆e
6 1 ad2antll ⊢G∈V∧K∈V∧K∈Vtx⁡G∧φ→∀n∈Vtx⁡G∖K¬∃e∈Edg⁡GKn⊆e
7 rabeq0 ⊢n∈Vtx⁡G∖K|∃e∈Edg⁡GKn⊆e=∅↔∀n∈Vtx⁡G∖K¬∃e∈Edg⁡GKn⊆e
8 6 7 sylibr ⊢G∈V∧K∈V∧K∈Vtx⁡G∧φ→n∈Vtx⁡G∖K|∃e∈Edg⁡GKn⊆e=∅
9 5 8 eqtrd ⊢G∈V∧K∈V∧K∈Vtx⁡G∧φ→GNeighbVtxK=∅
10 9 expcom ⊢K∈Vtx⁡G∧φ→G∈V∧K∈V→GNeighbVtxK=∅
11 10 ex ⊢K∈Vtx⁡G→φ→G∈V∧K∈V→GNeighbVtxK=∅
12 11 com23 ⊢K∈Vtx⁡G→G∈V∧K∈V→φ→GNeighbVtxK=∅
13 df-nel ⊢K∉Vtx⁡G↔¬K∈Vtx⁡G
14 2 nbgrnvtx0 ⊢K∉Vtx⁡G→GNeighbVtxK=∅
15 13 14 sylbir ⊢¬K∈Vtx⁡G→GNeighbVtxK=∅
16 15 a1d ⊢¬K∈Vtx⁡G→φ→GNeighbVtxK=∅
17 nbgrprc0 ⊢¬G∈V∧K∈V→GNeighbVtxK=∅
18 17 a1d ⊢¬G∈V∧K∈V→φ→GNeighbVtxK=∅
19 12 16 18 pm2.61nii ⊢φ→GNeighbVtxK=∅