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 
|- ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = U_ x e. ( 1 ... N ) { { 0 , x } } )

Proof

Step Hyp Ref Expression
1 stgredgel 
 |-  ( N e. NN0 -> ( e e. ( Edg ` ( StarGr ` N ) ) <-> ( e C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) e = { 0 , x } ) ) )
2 eliun 
 |-  ( e e. U_ x e. ( 1 ... N ) { { 0 , x } } <-> E. x e. ( 1 ... N ) e e. { { 0 , x } } )
3 2 a1i 
 |-  ( N e. NN0 -> ( e e. U_ x e. ( 1 ... N ) { { 0 , x } } <-> E. x e. ( 1 ... N ) e e. { { 0 , x } } ) )
4 velsn 
 |-  ( e e. { { 0 , x } } <-> e = { 0 , x } )
5 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
6 5 adantr 
 |-  ( ( N e. NN0 /\ x e. ( 1 ... N ) ) -> 0 e. ( 0 ... N ) )
7 fz1ssfz0 
 |-  ( 1 ... N ) C_ ( 0 ... N )
8 7 sseli 
 |-  ( x e. ( 1 ... N ) -> x e. ( 0 ... N ) )
9 8 adantl 
 |-  ( ( N e. NN0 /\ x e. ( 1 ... N ) ) -> x e. ( 0 ... N ) )
10 6 9 prssd 
 |-  ( ( N e. NN0 /\ x e. ( 1 ... N ) ) -> { 0 , x } C_ ( 0 ... N ) )
11 sseq1 
 |-  ( e = { 0 , x } -> ( e C_ ( 0 ... N ) <-> { 0 , x } C_ ( 0 ... N ) ) )
12 10 11 syl5ibrcom 
 |-  ( ( N e. NN0 /\ x e. ( 1 ... N ) ) -> ( e = { 0 , x } -> e C_ ( 0 ... N ) ) )
13 12 pm4.71rd 
 |-  ( ( N e. NN0 /\ x e. ( 1 ... N ) ) -> ( e = { 0 , x } <-> ( e C_ ( 0 ... N ) /\ e = { 0 , x } ) ) )
14 4 13 bitr2id 
 |-  ( ( N e. NN0 /\ x e. ( 1 ... N ) ) -> ( ( e C_ ( 0 ... N ) /\ e = { 0 , x } ) <-> e e. { { 0 , x } } ) )
15 14 rexbidva 
 |-  ( N e. NN0 -> ( E. x e. ( 1 ... N ) ( e C_ ( 0 ... N ) /\ e = { 0 , x } ) <-> E. x e. ( 1 ... N ) e e. { { 0 , x } } ) )
16 r19.42v 
 |-  ( E. x e. ( 1 ... N ) ( e C_ ( 0 ... N ) /\ e = { 0 , x } ) <-> ( e C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) e = { 0 , x } ) )
17 16 a1i 
 |-  ( N e. NN0 -> ( E. x e. ( 1 ... N ) ( e C_ ( 0 ... N ) /\ e = { 0 , x } ) <-> ( e C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) e = { 0 , x } ) ) )
18 3 15 17 3bitr2rd 
 |-  ( N e. NN0 -> ( ( e C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) e = { 0 , x } ) <-> e e. U_ x e. ( 1 ... N ) { { 0 , x } } ) )
19 1 18 bitrd 
 |-  ( N e. NN0 -> ( e e. ( Edg ` ( StarGr ` N ) ) <-> e e. U_ x e. ( 1 ... N ) { { 0 , x } } ) )
20 19 eqrdv 
 |-  ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = U_ x e. ( 1 ... N ) { { 0 , x } } )