Description: Alternate definition of the semiclosed neighborhood of a vertex breaking up the subset relationship of an unordered pair. Asemiclosed neighborhood S of a vertex N is the set of all vertices incident with edges which join the vertex N with a vertex. Therefore, a vertex is contained in its semiclosed neighborhood if it is connected with any vertex by an edge (see sclnbgrelself ), even only with itself (i.e., by a loop). (Contributed by AV, 16-May-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dfsclnbgr2.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| dfsclnbgr2.s | ⊢ 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } | ||
| dfsclnbgr2.e | ⊢ 𝐸 = ( Edg ‘ 𝐺 ) | ||
| Assertion | dfsclnbgr2 | ⊢ ( 𝑁 ∈ 𝑉 → 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfsclnbgr2.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| 2 | dfsclnbgr2.s | ⊢ 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } | |
| 3 | dfsclnbgr2.e | ⊢ 𝐸 = ( Edg ‘ 𝐺 ) | |
| 4 | prssg | ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ) | |
| 5 | 4 | bicomd | ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) ) |
| 6 | 5 | rexbidv | ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) ) |
| 7 | 6 | rabbidva | ⊢ ( 𝑁 ∈ 𝑉 → { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) |
| 8 | 2 7 | eqtrid | ⊢ ( 𝑁 ∈ 𝑉 → 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) |