Step |
Hyp |
Ref |
Expression |
1 |
|
stgrfv |
Could not format ( 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 } } ) >. } ) : No typesetting found for |- ( 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 } } ) >. } ) with typecode |- |
2 |
1
|
fveq2d |
Could not format ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) ) : No typesetting found for |- ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) ) with typecode |- |
3 |
|
ovex |
|
4 |
|
eqid |
|
5 |
|
pwexg |
|
6 |
4 5
|
rabexd |
|
7 |
6
|
resiexd |
|
8 |
3 7
|
ax-mp |
|
9 |
3 8
|
pm3.2i |
|
10 |
|
eqid |
|
11 |
10
|
struct2griedg |
|
12 |
9 11
|
mp1i |
|
13 |
2 12
|
eqtrd |
Could not format ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) : No typesetting found for |- ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) with typecode |- |