Step |
Hyp |
Ref |
Expression |
1 |
|
0nn0 |
|
2 |
|
stgrfv |
Could not format ( 0 e. NN0 -> ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } ) : No typesetting found for |- ( 0 e. NN0 -> ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } ) with typecode |- |
3 |
1 2
|
ax-mp |
Could not format ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } : No typesetting found for |- ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } with typecode |- |
4 |
|
fz0sn |
|
5 |
4
|
opeq2i |
|
6 |
|
rabeq0 |
|
7 |
|
noel |
|
8 |
7
|
pm2.21i |
|
9 |
|
fz10 |
|
10 |
8 9
|
eleq2s |
|
11 |
10
|
a1i |
|
12 |
11
|
ralrimiv |
|
13 |
|
ralnex |
|
14 |
12 13
|
sylib |
|
15 |
6 14
|
mprgbir |
|
16 |
15
|
reseq2i |
|
17 |
|
res0 |
|
18 |
16 17
|
eqtri |
|
19 |
18
|
opeq2i |
|
20 |
5 19
|
preq12i |
|
21 |
3 20
|
eqtri |
Could not format ( StarGr ` 0 ) = { <. ( Base ` ndx ) , { 0 } >. , <. ( .ef ` ndx ) , (/) >. } : No typesetting found for |- ( StarGr ` 0 ) = { <. ( Base ` ndx ) , { 0 } >. , <. ( .ef ` ndx ) , (/) >. } with typecode |- |