Step |
Hyp |
Ref |
Expression |
1 |
|
nbcplgr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
1
|
cplgruvtxb |
⊢ ( 𝐺 ∈ ComplGraph → ( 𝐺 ∈ ComplGraph ↔ ( UnivVtx ‘ 𝐺 ) = 𝑉 ) ) |
3 |
2
|
ibi |
⊢ ( 𝐺 ∈ ComplGraph → ( UnivVtx ‘ 𝐺 ) = 𝑉 ) |
4 |
3
|
eqcomd |
⊢ ( 𝐺 ∈ ComplGraph → 𝑉 = ( UnivVtx ‘ 𝐺 ) ) |
5 |
4
|
eleq2d |
⊢ ( 𝐺 ∈ ComplGraph → ( 𝑁 ∈ 𝑉 ↔ 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ) ) |
6 |
5
|
biimpa |
⊢ ( ( 𝐺 ∈ ComplGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ) |
7 |
1
|
uvtxnbgrb |
⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝐺 NeighbVtx 𝑁 ) = ( 𝑉 ∖ { 𝑁 } ) ) ) |
8 |
7
|
adantl |
⊢ ( ( 𝐺 ∈ ComplGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝐺 NeighbVtx 𝑁 ) = ( 𝑉 ∖ { 𝑁 } ) ) ) |
9 |
6 8
|
mpbid |
⊢ ( ( 𝐺 ∈ ComplGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = ( 𝑉 ∖ { 𝑁 } ) ) |