Step |
Hyp |
Ref |
Expression |
1 |
|
clnbgrval.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
clnbgrval.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
1 2
|
clnbgrval |
⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) ) |
4 |
|
prssg |
⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ V ) → ( ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ) |
5 |
4
|
elvd |
⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ) |
6 |
5
|
bicomd |
⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) ) |
7 |
6
|
rexbidv |
⊢ ( 𝑁 ∈ 𝑉 → ( ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ) ) |
8 |
7
|
rabbidv |
⊢ ( 𝑁 ∈ 𝑉 → { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) |
9 |
8
|
uneq2d |
⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) ) |
10 |
3 9
|
eqtrd |
⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) ) |