Step |
Hyp |
Ref |
Expression |
1 |
|
df-stgr |
|- StarGr = ( n e. NN0 |-> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } ) |
2 |
1
|
a1i |
|- ( N e. NN0 -> StarGr = ( n e. NN0 |-> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } ) ) |
3 |
|
oveq2 |
|- ( n = N -> ( 0 ... n ) = ( 0 ... N ) ) |
4 |
3
|
opeq2d |
|- ( n = N -> <. ( Base ` ndx ) , ( 0 ... n ) >. = <. ( Base ` ndx ) , ( 0 ... N ) >. ) |
5 |
3
|
pweqd |
|- ( n = N -> ~P ( 0 ... n ) = ~P ( 0 ... N ) ) |
6 |
|
oveq2 |
|- ( n = N -> ( 1 ... n ) = ( 1 ... N ) ) |
7 |
6
|
rexeqdv |
|- ( n = N -> ( E. x e. ( 1 ... n ) e = { 0 , x } <-> E. x e. ( 1 ... N ) e = { 0 , x } ) ) |
8 |
5 7
|
rabeqbidv |
|- ( n = N -> { 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 } } ) |
9 |
8
|
reseq2d |
|- ( n = N -> ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) = ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) |
10 |
9
|
opeq2d |
|- ( n = N -> <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. = <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. ) |
11 |
4 10
|
preq12d |
|- ( n = N -> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } = { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) |
12 |
11
|
adantl |
|- ( ( N e. NN0 /\ n = N ) -> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } = { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) |
13 |
|
id |
|- ( N e. NN0 -> N e. NN0 ) |
14 |
|
prex |
|- { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } e. _V |
15 |
14
|
a1i |
|- ( N e. NN0 -> { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } e. _V ) |
16 |
2 12 13 15
|
fvmptd |
|- ( N e. NN0 -> ( StarGr ` N ) = { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) |