Metamath Proof Explorer

Theorem stgredgiun

Description: The edges of the star graph S_N as indexed union. (Contributed by AV, 29-Sep-2025)

Ref Expression
Assertion stgredgiun ( 𝑁 ∈ ℕ0 → ( Edg ‘ ( StarGr ‘ 𝑁 ) ) = ∪ 𝑥 ∈ ( 1 ... 𝑁 ) { { 0 , 𝑥 } } )

Proof

Step Hyp Ref Expression
1 stgredgel ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑒 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ↔ ( 𝑒 ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } ) ) )
2 eliun ⊢ ( 𝑒 ∈ ∪ 𝑥 ∈ ( 1 ... 𝑁 ) { { 0 , 𝑥 } } ↔ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 ∈ { { 0 , 𝑥 } } )
3 2 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑒 ∈ ∪ 𝑥 ∈ ( 1 ... 𝑁 ) { { 0 , 𝑥 } } ↔ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 ∈ { { 0 , 𝑥 } } ) )
4 velsn ⊢ ( 𝑒 ∈ { { 0 , 𝑥 } } ↔ 𝑒 = { 0 , 𝑥 } )
5 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
6 5 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → 0 ∈ ( 0 ... 𝑁 ) )
7 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
8 7 sseli ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 𝑥 ∈ ( 0 ... 𝑁 ) )
9 8 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → 𝑥 ∈ ( 0 ... 𝑁 ) )
10 6 9 prssd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → { 0 , 𝑥 } ⊆ ( 0 ... 𝑁 ) )
11 sseq1 ⊢ ( 𝑒 = { 0 , 𝑥 } → ( 𝑒 ⊆ ( 0 ... 𝑁 ) ↔ { 0 , 𝑥 } ⊆ ( 0 ... 𝑁 ) ) )
12 10 11 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( 𝑒 = { 0 , 𝑥 } → 𝑒 ⊆ ( 0 ... 𝑁 ) ) )
13 12 pm4.71rd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( 𝑒 = { 0 , 𝑥 } ↔ ( 𝑒 ⊆ ( 0 ... 𝑁 ) ∧ 𝑒 = { 0 , 𝑥 } ) ) )
14 4 13 bitr2id ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑒 ⊆ ( 0 ... 𝑁 ) ∧ 𝑒 = { 0 , 𝑥 } ) ↔ 𝑒 ∈ { { 0 , 𝑥 } } ) )
15 14 rexbidva ⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑥 ∈ ( 1 ... 𝑁 ) ( 𝑒 ⊆ ( 0 ... 𝑁 ) ∧ 𝑒 = { 0 , 𝑥 } ) ↔ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 ∈ { { 0 , 𝑥 } } ) )
16 r19.42v ⊢ ( ∃ 𝑥 ∈ ( 1 ... 𝑁 ) ( 𝑒 ⊆ ( 0 ... 𝑁 ) ∧ 𝑒 = { 0 , 𝑥 } ) ↔ ( 𝑒 ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } ) )
17 16 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑥 ∈ ( 1 ... 𝑁 ) ( 𝑒 ⊆ ( 0 ... 𝑁 ) ∧ 𝑒 = { 0 , 𝑥 } ) ↔ ( 𝑒 ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } ) ) )
18 3 15 17 3bitr2rd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑒 ⊆ ( 0 ... 𝑁 ) ∧ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } ) ↔ 𝑒 ∈ ∪ 𝑥 ∈ ( 1 ... 𝑁 ) { { 0 , 𝑥 } } ) )
19 1 18 bitrd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑒 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ↔ 𝑒 ∈ ∪ 𝑥 ∈ ( 1 ... 𝑁 ) { { 0 , 𝑥 } } ) )
20 19 eqrdv ⊢ ( 𝑁 ∈ ℕ0 → ( Edg ‘ ( StarGr ‘ 𝑁 ) ) = ∪ 𝑥 ∈ ( 1 ... 𝑁 ) { { 0 , 𝑥 } } )