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 |- |