Step |
Hyp |
Ref |
Expression |
1 |
|
cplgruvtxb.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
1
|
iscplgr |
⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) ) |
3 |
1
|
uvtxel |
⊢ ( 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) |
4 |
3
|
a1i |
⊢ ( 𝐺 ∈ 𝑊 → ( 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) ) |
5 |
4
|
baibd |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) |
6 |
5
|
ralbidva |
⊢ ( 𝐺 ∈ 𝑊 → ( ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) |
7 |
2 6
|
bitrd |
⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) |