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 Could not format assertion : No typesetting found for |- ( StarGr ` 0 ) = { <. ( Base ` ndx ) , { 0 } >. , <. ( .ef ` ndx ) , (/) >. } with typecode |-

Proof

Step Hyp Ref Expression
1 0nn0 0 0
2 stgrfv Could not format ( 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 } } ) >. } ) : No typesetting found for |- ( 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 } } ) >. } ) with typecode |-
3 1 2 ax-mp Could not format ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } : No typesetting found for |- ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } with typecode |-
4 fz0sn 0 0 = 0
5 4 opeq2i Base ndx 0 0 = Base ndx 0
6 rabeq0 e 𝒫 0 0 | x 1 0 e = 0 x = e 𝒫 0 0 ¬ x 1 0 e = 0 x
7 noel ¬ x
8 7 pm2.21i x ¬ e = 0 x
9 fz10 1 0 =
10 8 9 eleq2s x 1 0 ¬ e = 0 x
11 10 a1i e 𝒫 0 0 x 1 0 ¬ e = 0 x
12 11 ralrimiv e 𝒫 0 0 x 1 0 ¬ e = 0 x
13 ralnex x 1 0 ¬ e = 0 x ¬ x 1 0 e = 0 x
14 12 13 sylib e 𝒫 0 0 ¬ x 1 0 e = 0 x
15 6 14 mprgbir e 𝒫 0 0 | x 1 0 e = 0 x =
16 15 reseq2i I e 𝒫 0 0 | x 1 0 e = 0 x = I
17 res0 I =
18 16 17 eqtri I e 𝒫 0 0 | x 1 0 e = 0 x =
19 18 opeq2i ef ndx I e 𝒫 0 0 | x 1 0 e = 0 x = ef ndx
20 5 19 preq12i Base ndx 0 0 ef ndx I e 𝒫 0 0 | x 1 0 e = 0 x = Base ndx 0 ef ndx
21 3 20 eqtri Could not format ( StarGr ` 0 ) = { <. ( Base ` ndx ) , { 0 } >. , <. ( .ef ` ndx ) , (/) >. } : No typesetting found for |- ( StarGr ` 0 ) = { <. ( Base ` ndx ) , { 0 } >. , <. ( .ef ` ndx ) , (/) >. } with typecode |-