| Step |
Hyp |
Ref |
Expression |
| 1 |
|
f1oi |
|
| 2 |
|
f1of1 |
|
| 3 |
1 2
|
mp1i |
|
| 4 |
|
simpllr |
|
| 5 |
|
fveq2 |
|
| 6 |
|
0red |
|
| 7 |
|
elfznn |
|
| 8 |
7
|
nngt0d |
|
| 9 |
6 8
|
ltned |
|
| 10 |
|
c0ex |
|
| 11 |
|
vex |
|
| 12 |
10 11
|
pm3.2i |
|
| 13 |
|
hashprg |
|
| 14 |
12 13
|
mp1i |
|
| 15 |
9 14
|
mpbid |
|
| 16 |
15
|
adantl |
|
| 17 |
5 16
|
sylan9eqr |
|
| 18 |
4 17
|
jca |
|
| 19 |
18
|
ex |
|
| 20 |
19
|
rexlimdva |
|
| 21 |
20
|
expimpd |
|
| 22 |
|
eqeq1 |
|
| 23 |
22
|
rexbidv |
|
| 24 |
23
|
elrab |
|
| 25 |
|
fveqeq2 |
|
| 26 |
25
|
elrab |
|
| 27 |
21 24 26
|
3imtr4g |
|
| 28 |
27
|
ssrdv |
|
| 29 |
|
f1ss |
|
| 30 |
3 28 29
|
syl2anc |
|
| 31 |
|
stgriedg |
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 |- |
| 32 |
31
|
dmeqd |
Could not format ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = dom ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) : No typesetting found for |- ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = dom ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) with typecode |- |
| 33 |
|
dmresi |
|
| 34 |
32 33
|
eqtrdi |
Could not format ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : No typesetting found for |- ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) with typecode |- |
| 35 |
|
stgrvtx |
Could not format ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) : No typesetting found for |- ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) with typecode |- |
| 36 |
35
|
pweqd |
Could not format ( N e. NN0 -> ~P ( Vtx ` ( StarGr ` N ) ) = ~P ( 0 ... N ) ) : No typesetting found for |- ( N e. NN0 -> ~P ( Vtx ` ( StarGr ` N ) ) = ~P ( 0 ... N ) ) with typecode |- |
| 37 |
36
|
rabeqdv |
Could not format ( N e. NN0 -> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } = { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) : No typesetting found for |- ( N e. NN0 -> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } = { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) with typecode |- |
| 38 |
31 34 37
|
f1eq123d |
Could not format ( N e. NN0 -> ( ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } <-> ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-> { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) ) : No typesetting found for |- ( N e. NN0 -> ( ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } <-> ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-> { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) ) with typecode |- |
| 39 |
30 38
|
mpbird |
Could not format ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) : No typesetting found for |- ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) with typecode |- |
| 40 |
|
fvex |
Could not format ( StarGr ` N ) e. _V : No typesetting found for |- ( StarGr ` N ) e. _V with typecode |- |
| 41 |
|
eqid |
Could not format ( Vtx ` ( StarGr ` N ) ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- ( Vtx ` ( StarGr ` N ) ) = ( Vtx ` ( StarGr ` N ) ) with typecode |- |
| 42 |
|
eqid |
Could not format ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` ( StarGr ` N ) ) : No typesetting found for |- ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` ( StarGr ` N ) ) with typecode |- |
| 43 |
41 42
|
isusgrs |
Could not format ( ( StarGr ` N ) e. _V -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) : No typesetting found for |- ( ( StarGr ` N ) e. _V -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) with typecode |- |
| 44 |
40 43
|
mp1i |
Could not format ( N e. NN0 -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) : No typesetting found for |- ( N e. NN0 -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) with typecode |- |
| 45 |
39 44
|
mpbird |
Could not format ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) : No typesetting found for |- ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) with typecode |- |