Step |
Hyp |
Ref |
Expression |
1 |
|
stgredgel |
Could not format ( N e. NN0 -> ( e e. ( Edg ` ( StarGr ` N ) ) <-> ( e C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) e = { 0 , x } ) ) ) : No typesetting found for |- ( N e. NN0 -> ( e e. ( Edg ` ( StarGr ` N ) ) <-> ( e C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) e = { 0 , x } ) ) ) with typecode |- |
2 |
|
eliun |
|
3 |
2
|
a1i |
|
4 |
|
velsn |
|
5 |
|
0elfz |
|
6 |
5
|
adantr |
|
7 |
|
fz1ssfz0 |
|
8 |
7
|
sseli |
|
9 |
8
|
adantl |
|
10 |
6 9
|
prssd |
|
11 |
|
sseq1 |
|
12 |
10 11
|
syl5ibrcom |
|
13 |
12
|
pm4.71rd |
|
14 |
4 13
|
bitr2id |
|
15 |
14
|
rexbidva |
|
16 |
|
r19.42v |
|
17 |
16
|
a1i |
|
18 |
3 15 17
|
3bitr2rd |
|
19 |
1 18
|
bitrd |
Could not format ( N e. NN0 -> ( e e. ( Edg ` ( StarGr ` N ) ) <-> e e. U_ x e. ( 1 ... N ) { { 0 , x } } ) ) : No typesetting found for |- ( N e. NN0 -> ( e e. ( Edg ` ( StarGr ` N ) ) <-> e e. U_ x e. ( 1 ... N ) { { 0 , x } } ) ) with typecode |- |
20 |
19
|
eqrdv |
Could not format ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = U_ x e. ( 1 ... N ) { { 0 , x } } ) : No typesetting found for |- ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = U_ x e. ( 1 ... N ) { { 0 , x } } ) with typecode |- |