| Step |
Hyp |
Ref |
Expression |
| 1 |
|
stgrfv |
|- ( N e. NN0 -> ( StarGr ` N ) = { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) |
| 2 |
1
|
fveq2d |
|- ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( Vtx ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) ) |
| 3 |
|
ovex |
|- ( 0 ... N ) e. _V |
| 4 |
|
eqid |
|- { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } |
| 5 |
|
pwexg |
|- ( ( 0 ... N ) e. _V -> ~P ( 0 ... N ) e. _V ) |
| 6 |
4 5
|
rabexd |
|- ( ( 0 ... N ) e. _V -> { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } e. _V ) |
| 7 |
6
|
resiexd |
|- ( ( 0 ... N ) e. _V -> ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) e. _V ) |
| 8 |
3 7
|
ax-mp |
|- ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) e. _V |
| 9 |
3 8
|
pm3.2i |
|- ( ( 0 ... N ) e. _V /\ ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) e. _V ) |
| 10 |
|
eqid |
|- { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } = { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } |
| 11 |
10
|
struct2grvtx |
|- ( ( ( 0 ... N ) e. _V /\ ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) e. _V ) -> ( Vtx ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) = ( 0 ... N ) ) |
| 12 |
9 11
|
mp1i |
|- ( N e. NN0 -> ( Vtx ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) = ( 0 ... N ) ) |
| 13 |
2 12
|
eqtrd |
|- ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) |