Theorem stgredg

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

	Ref	Expression
Assertion	stgredg	⊢ ( 𝑁 ∈ ℕ0 → ( Edg ‘ ( StarGr ‘ 𝑁 ) ) = { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } )

Proof

Step	Hyp	Ref	Expression
1		edgval	⊢ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) = ran ( iEdg ‘ ( StarGr ‘ 𝑁 ) )
2		stgriedg	⊢ ( 𝑁 ∈ ℕ0 → ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) = ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) )
3	2	rneqd	⊢ ( 𝑁 ∈ ℕ0 → ran ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) = ran ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) )
4		rnresi	⊢ ran ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) = { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } }
5	3 4	eqtrdi	⊢ ( 𝑁 ∈ ℕ0 → ran ( iEdg ‘ ( StarGr ‘ 𝑁 ) ) = { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } )
6	1 5	eqtrid	⊢ ( 𝑁 ∈ ℕ0 → ( Edg ‘ ( StarGr ‘ 𝑁 ) ) = { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } )