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 ∈ ℕ0
2		stgrfv	⊢ ( 0 ∈ ℕ0 → ( StarGr ‘ 0 ) = { ⟨ ( Base ‘ ndx ) , ( 0 ... 0 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )
3	1 2	ax-mp	⊢ ( StarGr ‘ 0 ) = { ⟨ ( Base ‘ ndx ) , ( 0 ... 0 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ }
4		fz0sn	⊢ ( 0 ... 0 ) = { 0 }
5	4	opeq2i	⊢ ⟨ ( Base ‘ ndx ) , ( 0 ... 0 ) ⟩ = ⟨ ( Base ‘ ndx ) , { 0 } ⟩
6		rabeq0	⊢ ( { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } = ∅ ↔ ∀ 𝑒 ∈ 𝒫 ( 0 ... 0 ) ¬ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } )
7		noel	⊢ ¬ 𝑥 ∈ ∅
8	7	pm2.21i	⊢ ( 𝑥 ∈ ∅ → ¬ 𝑒 = { 0 , 𝑥 } )
9		fz10	⊢ ( 1 ... 0 ) = ∅
10	8 9	eleq2s	⊢ ( 𝑥 ∈ ( 1 ... 0 ) → ¬ 𝑒 = { 0 , 𝑥 } )
11	10	a1i	⊢ ( 𝑒 ∈ 𝒫 ( 0 ... 0 ) → ( 𝑥 ∈ ( 1 ... 0 ) → ¬ 𝑒 = { 0 , 𝑥 } ) )
12	11	ralrimiv	⊢ ( 𝑒 ∈ 𝒫 ( 0 ... 0 ) → ∀ 𝑥 ∈ ( 1 ... 0 ) ¬ 𝑒 = { 0 , 𝑥 } )
13		ralnex	⊢ ( ∀ 𝑥 ∈ ( 1 ... 0 ) ¬ 𝑒 = { 0 , 𝑥 } ↔ ¬ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } )
14	12 13	sylib	⊢ ( 𝑒 ∈ 𝒫 ( 0 ... 0 ) → ¬ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } )
15	6 14	mprgbir	⊢ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } = ∅
16	15	reseq2i	⊢ ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) = ( I ↾ ∅ )
17		res0	⊢ ( I ↾ ∅ ) = ∅
18	16 17	eqtri	⊢ ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) = ∅
19	18	opeq2i	⊢ ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ = ⟨ ( .ef ‘ ndx ) , ∅ ⟩
20	5 19	preq12i	⊢ { ⟨ ( Base ‘ ndx ) , ( 0 ... 0 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 0 ) ∣ ∃ 𝑥 ∈ ( 1 ... 0 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } = { ⟨ ( Base ‘ ndx ) , { 0 } ⟩ , ⟨ ( .ef ‘ ndx ) , ∅ ⟩ }
21	3 20	eqtri	⊢ ( StarGr ‘ 0 ) = { ⟨ ( Base ‘ ndx ) , { 0 } ⟩ , ⟨ ( .ef ‘ ndx ) , ∅ ⟩ }