Step |
Hyp |
Ref |
Expression |
1 |
|
gpgov.j |
|
2 |
|
gpgov.i |
|
3 |
1 2
|
gpgov |
Could not format ( ( N e. NN /\ K e. J ) -> ( N gPetersenGr K ) = { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( N gPetersenGr K ) = { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) with typecode |- |
4 |
3
|
fveq2d |
Could not format ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( Vtx ` { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) ) : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( Vtx ` { <. ( Base ` ndx ) , ( { 0 , 1 } X. I ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. I ) | E. x e. I ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) } ) >. } ) ) with typecode |- |
5 |
|
prex |
|
6 |
2
|
ovexi |
|
7 |
5 6
|
xpex |
|
8 |
|
eqid |
|
9 |
5
|
a1i |
|
10 |
|
ovexd |
|
11 |
2 10
|
eqeltrid |
|
12 |
9 11
|
xpexd |
|
13 |
12
|
pwexd |
|
14 |
8 13
|
rabexd |
|
15 |
14
|
resiexd |
|
16 |
2 15
|
ax-mp |
|
17 |
7 16
|
pm3.2i |
|
18 |
|
eqid |
|
19 |
18
|
struct2grvtx |
|
20 |
17 19
|
mp1i |
|
21 |
4 20
|
eqtrd |
Could not format ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. I ) ) : No typesetting found for |- ( ( N e. NN /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. I ) ) with typecode |- |