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 Could not format assertion : No typesetting found for |- ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = U_ x e. ( 1 ... N ) { { 0 , x } } ) with typecode |-

Proof

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