Metamath Proof Explorer

Theorem stgr0

Description: The star graph S_0 consists of a single vertex without edges. (Contributed by AV, 11-Sep-2025)

Ref Expression
Assertion stgr0 
|- ( StarGr ` 0 ) = { <. ( Base ` ndx ) , { 0 } >. , <. ( .ef ` ndx ) , (/) >. }

Proof

Step Hyp Ref Expression
1 0nn0 
 |-  0 e. NN0
2 stgrfv 
 |-  ( 0 e. NN0 -> ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } )
3 1 2 ax-mp 
 |-  ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. }
4 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
5 4 opeq2i 
 |-  <. ( Base ` ndx ) , ( 0 ... 0 ) >. = <. ( Base ` ndx ) , { 0 } >.
6 rabeq0 
 |-  ( { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } = (/) <-> A. e e. ~P ( 0 ... 0 ) -. E. x e. ( 1 ... 0 ) e = { 0 , x } )
7 noel 
 |-  -. x e. (/)
8 7 pm2.21i 
 |-  ( x e. (/) -> -. e = { 0 , x } )
9 fz10 
 |-  ( 1 ... 0 ) = (/)
10 8 9 eleq2s 
 |-  ( x e. ( 1 ... 0 ) -> -. e = { 0 , x } )
11 10 a1i 
 |-  ( e e. ~P ( 0 ... 0 ) -> ( x e. ( 1 ... 0 ) -> -. e = { 0 , x } ) )
12 11 ralrimiv 
 |-  ( e e. ~P ( 0 ... 0 ) -> A. x e. ( 1 ... 0 ) -. e = { 0 , x } )
13 ralnex 
 |-  ( A. x e. ( 1 ... 0 ) -. e = { 0 , x } <-> -. E. x e. ( 1 ... 0 ) e = { 0 , x } )
14 12 13 sylib 
 |-  ( e e. ~P ( 0 ... 0 ) -> -. E. x e. ( 1 ... 0 ) e = { 0 , x } )
15 6 14 mprgbir 
 |-  { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } = (/)
16 15 reseq2i 
 |-  ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) = ( _I |` (/) )
17 res0 
 |-  ( _I |` (/) ) = (/)
18 16 17 eqtri 
 |-  ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) = (/)
19 18 opeq2i 
 |-  <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. = <. ( .ef ` ndx ) , (/) >.
20 5 19 preq12i 
 |-  { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } = { <. ( Base ` ndx ) , { 0 } >. , <. ( .ef ` ndx ) , (/) >. }
21 3 20 eqtri 
 |-  ( StarGr ` 0 ) = { <. ( Base ` ndx ) , { 0 } >. , <. ( .ef ` ndx ) , (/) >. }