Metamath Proof Explorer


Definition df-stgr

Description: Definition of star graphs according to the first definition in Wikipedia, so that ( StarGrN ) has size N , and order N + 1 : ( StarGr0 ) will be a single vertex (graph without edges), see stgr0 , ( StarGr1 ) will be a single edge (graph with two vertices connected by an edge), see stgr1 , and ( StarGr3 ) will be a 3-star or "claw" (a star with 3 edges). (Contributed by AV, 10-Sep-2025)

Ref Expression
Assertion df-stgr StarGr = ( 𝑛 ∈ ℕ0 ↦ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstgr StarGr
1 vn 𝑛
2 cn0 0
3 cbs Base
4 cnx ndx
5 4 3 cfv ( Base ‘ ndx )
6 cc0 0
7 cfz ...
8 1 cv 𝑛
9 6 8 7 co ( 0 ... 𝑛 )
10 5 9 cop ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩
11 cedgf .ef
12 4 11 cfv ( .ef ‘ ndx )
13 cid I
14 ve 𝑒
15 9 cpw 𝒫 ( 0 ... 𝑛 )
16 vx 𝑥
17 c1 1
18 17 8 7 co ( 1 ... 𝑛 )
19 14 cv 𝑒
20 16 cv 𝑥
21 6 20 cpr { 0 , 𝑥 }
22 19 21 wceq 𝑒 = { 0 , 𝑥 }
23 22 16 18 wrex 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 }
24 23 14 15 crab { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } }
25 13 24 cres ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } )
26 12 25 cop ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩
27 10 26 cpr { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ }
28 1 2 27 cmpt ( 𝑛 ∈ ℕ0 ↦ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )
29 0 28 wceq StarGr = ( 𝑛 ∈ ℕ0 ↦ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )