Description: The vertices connected by an edge are a subset of the neighborhood of each of these vertices. (Contributed by AV, 26-May-2025) (Proof shortened by AV, 24-Aug-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | clnbgrssedg.e | ⊢ 𝐸 = ( Edg ‘ 𝐺 ) | |
| clnbgrssedg.n | ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑋 ) | ||
| Assertion | clnbgrssedg | ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ) → 𝐾 ⊆ 𝑁 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | clnbgrssedg.e | ⊢ 𝐸 = ( Edg ‘ 𝐺 ) | |
| 2 | clnbgrssedg.n | ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑋 ) | |
| 3 | 1 2 | clnbgredg | ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑣 ∈ 𝐾 ) ) → 𝑣 ∈ 𝑁 ) |
| 4 | 3 | 3exp2 | ⊢ ( 𝐺 ∈ UHGraph → ( 𝐾 ∈ 𝐸 → ( 𝑋 ∈ 𝐾 → ( 𝑣 ∈ 𝐾 → 𝑣 ∈ 𝑁 ) ) ) ) |
| 5 | 4 | 3imp | ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ) → ( 𝑣 ∈ 𝐾 → 𝑣 ∈ 𝑁 ) ) |
| 6 | 5 | ssrdv | ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ) → 𝐾 ⊆ 𝑁 ) |