Description: In a null graph (with no vertices), all neighborhoods are empty. (Contributed by AV, 15-Nov-2020) (Proof shortened by AV, 10-May-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nbgr0vtx | ⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( 𝐺 NeighbVtx 𝐾 ) = ∅ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nel02 | ⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ¬ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) | |
| 2 | df-nel | ⊢ ( 𝐾 ∉ ( Vtx ‘ 𝐺 ) ↔ ¬ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) | |
| 3 | 1 2 | sylibr | ⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → 𝐾 ∉ ( Vtx ‘ 𝐺 ) ) |
| 4 | eqid | ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) | |
| 5 | 4 | nbgrnvtx0 | ⊢ ( 𝐾 ∉ ( Vtx ‘ 𝐺 ) → ( 𝐺 NeighbVtx 𝐾 ) = ∅ ) |
| 6 | 3 5 | syl | ⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( 𝐺 NeighbVtx 𝐾 ) = ∅ ) |