Step |
Hyp |
Ref |
Expression |
1 |
|
opgpgvtx.i |
|
2 |
|
opgpgvtx.j |
|
3 |
|
opgpgvtx.g |
Could not format G = ( N gPetersenGr K ) : No typesetting found for |- G = ( N gPetersenGr K ) with typecode |- |
4 |
|
opgpgvtx.v |
|
5 |
3
|
fveq2i |
Could not format ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) ) : No typesetting found for |- ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) ) with typecode |- |
6 |
4 5
|
eqtri |
Could not format V = ( Vtx ` ( N gPetersenGr K ) ) : No typesetting found for |- V = ( Vtx ` ( N gPetersenGr K ) ) with typecode |- |
7 |
|
eluzge3nn |
|
8 |
2 1
|
gpgvtx |
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 |- |
9 |
7 8
|
sylan |
Could not format ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. I ) ) : No typesetting found for |- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. I ) ) with typecode |- |
10 |
6 9
|
eqtrid |
|
11 |
10
|
eleq2d |
|
12 |
|
opelxp |
|
13 |
12
|
a1i |
|
14 |
|
c0ex |
|
15 |
|
1ex |
|
16 |
14 15
|
elpr2 |
|
17 |
16
|
a1i |
|
18 |
17
|
anbi1d |
|
19 |
11 13 18
|
3bitrd |
|