Metamath Proof Explorer

Theorem stgrfv

Description: The star graph S_N. (Contributed by AV, 10-Sep-2025)

		Ref	Expression
	Assertion	stgrfv	⊢ ( 𝑁 ∈ ℕ₀ → ( StarGr ‘ 𝑁 ) = { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		df-stgr	⊢ StarGr = ( 𝑛 ∈ ℕ₀ ↦ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )
2	1	a1i	⊢ ( 𝑁 ∈ ℕ₀ → StarGr = ( 𝑛 ∈ ℕ₀ ↦ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } ) )
3		oveq2	⊢ ( 𝑛 = 𝑁 → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
4	3	opeq2d	⊢ ( 𝑛 = 𝑁 → ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ = ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ )
5	3	pweqd	⊢ ( 𝑛 = 𝑁 → 𝒫 ( 0 ... 𝑛 ) = 𝒫 ( 0 ... 𝑁 ) )
6		oveq2	⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
7	6	rexeqdv	⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } ↔ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } ) )
8	5 7	rabeqbidv	⊢ ( 𝑛 = 𝑁 → { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } = { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } )
9	8	reseq2d	⊢ ( 𝑛 = 𝑁 → ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) = ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) )
10	9	opeq2d	⊢ ( 𝑛 = 𝑁 → ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ = ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ )
11	4 10	preq12d	⊢ ( 𝑛 = 𝑁 → { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )
12	11	adantl	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ 𝑛 = 𝑁 ) → { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )
13		id	⊢ ( 𝑁 ∈ ℕ₀ → 𝑁 ∈ ℕ₀ )
14		prex	⊢ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } ∈ V
15	14	a1i	⊢ ( 𝑁 ∈ ℕ₀ → { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } ∈ V )
16	2 12 13 15	fvmptd	⊢ ( 𝑁 ∈ ℕ₀ → ( StarGr ‘ 𝑁 ) = { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )