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 , 𝑥 } } )