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 ( 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 ) , ∅ ⟩ }