Metamath Proof Explorer

Theorem nbgr0edglem

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

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

Proof

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