Metamath Proof Explorer


Theorem stgriedg

Description: The indexed edges of the star graph S_N. (Contributed by AV, 11-Sep-2025)

Ref Expression
Assertion stgriedg Could not format assertion : 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 |-

Proof

Step Hyp Ref Expression
1 stgrfv Could not format ( 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 } } ) >. } ) : No typesetting found for |- ( 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 } } ) >. } ) with typecode |-
2 1 fveq2d Could not format ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) ) : No typesetting found for |- ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) ) with typecode |-
3 ovex 0 N V
4 eqid e 𝒫 0 N | x 1 N e = 0 x = e 𝒫 0 N | x 1 N e = 0 x
5 pwexg 0 N V 𝒫 0 N V
6 4 5 rabexd 0 N V e 𝒫 0 N | x 1 N e = 0 x V
7 6 resiexd 0 N V I e 𝒫 0 N | x 1 N e = 0 x V
8 3 7 ax-mp I e 𝒫 0 N | x 1 N e = 0 x V
9 3 8 pm3.2i 0 N V I e 𝒫 0 N | x 1 N e = 0 x V
10 eqid Base ndx 0 N ef ndx I e 𝒫 0 N | x 1 N e = 0 x = Base ndx 0 N ef ndx I e 𝒫 0 N | x 1 N e = 0 x
11 10 struct2griedg 0 N V I e 𝒫 0 N | x 1 N e = 0 x V iEdg Base ndx 0 N ef ndx I e 𝒫 0 N | x 1 N e = 0 x = I e 𝒫 0 N | x 1 N e = 0 x
12 9 11 mp1i N 0 iEdg Base ndx 0 N ef ndx I e 𝒫 0 N | x 1 N e = 0 x = I e 𝒫 0 N | x 1 N e = 0 x
13 2 12 eqtrd 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 |-