Description: The vertices connected by an edge are a subset of the neigborhood 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 ∧ 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ) → 𝐾 ⊆ 𝑁 ) |