Metamath Proof Explorer


Theorem stgrorder

Description: The order of a star graph S_N. (Contributed by AV, 12-Sep-2025)

Ref Expression
Hypotheses stgrvtx0.g 𝐺 = ( StarGr ‘ 𝑁 )
stgrvtx0.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion stgrorder ( 𝑁 ∈ ℕ0 → ( ♯ ‘ 𝑉 ) = ( 𝑁 + 1 ) )

Proof

Step Hyp Ref Expression
1 stgrvtx0.g 𝐺 = ( StarGr ‘ 𝑁 )
2 stgrvtx0.v 𝑉 = ( Vtx ‘ 𝐺 )
3 1 fveq2i ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
4 2 3 eqtri 𝑉 = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
5 stgrvtx ( 𝑁 ∈ ℕ0 → ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( 0 ... 𝑁 ) )
6 4 5 eqtrid ( 𝑁 ∈ ℕ0𝑉 = ( 0 ... 𝑁 ) )
7 6 fveq2d ( 𝑁 ∈ ℕ0 → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ ( 0 ... 𝑁 ) ) )
8 hashfz0 ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ... 𝑁 ) ) = ( 𝑁 + 1 ) )
9 7 8 eqtrd ( 𝑁 ∈ ℕ0 → ( ♯ ‘ 𝑉 ) = ( 𝑁 + 1 ) )