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 | |- E = ( Edg ` G ) |
|
clnbgrssedg.n | |- N = ( G ClNeighbVtx X ) |
||
Assertion | clnbgrssedg | |- ( ( G e. UHGraph /\ K e. E /\ X e. K ) -> K C_ N ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clnbgrssedg.e | |- E = ( Edg ` G ) |
|
2 | clnbgrssedg.n | |- N = ( G ClNeighbVtx X ) |
|
3 | 1 2 | clnbgredg | |- ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ v e. K ) ) -> v e. N ) |
4 | 3 | 3exp2 | |- ( G e. UHGraph -> ( K e. E -> ( X e. K -> ( v e. K -> v e. N ) ) ) ) |
5 | 4 | 3imp | |- ( ( G e. UHGraph /\ K e. E /\ X e. K ) -> ( v e. K -> v e. N ) ) |
6 | 5 | ssrdv | |- ( ( G e. UHGraph /\ K e. E /\ X e. K ) -> K C_ N ) |