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