Metamath Proof Explorer

Theorem stgredgel

Description: An edge of the star graph S_N. (Contributed by AV, 11-Sep-2025)

Ref Expression
Assertion stgredgel 
|- ( N e. NN0 -> ( E e. ( Edg ` ( StarGr ` N ) ) <-> ( E C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) E = { 0 , x } ) ) )

Proof

Step Hyp Ref Expression
1 stgredg 
 |-  ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } )
2 1 eleq2d 
 |-  ( N e. NN0 -> ( E e. ( Edg ` ( StarGr ` N ) ) <-> E e. { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) )
3 eqeq1 
 |-  ( e = E -> ( e = { 0 , x } <-> E = { 0 , x } ) )
4 3 rexbidv 
 |-  ( e = E -> ( E. x e. ( 1 ... N ) e = { 0 , x } <-> E. x e. ( 1 ... N ) E = { 0 , x } ) )
5 4 elrab 
 |-  ( E e. { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } <-> ( E e. ~P ( 0 ... N ) /\ E. x e. ( 1 ... N ) E = { 0 , x } ) )
6 prex 
 |-  { 0 , x } e. _V
7 eleq1 
 |-  ( E = { 0 , x } -> ( E e. _V <-> { 0 , x } e. _V ) )
8 6 7 mpbiri 
 |-  ( E = { 0 , x } -> E e. _V )
9 elpwg 
 |-  ( E e. _V -> ( E e. ~P ( 0 ... N ) <-> E C_ ( 0 ... N ) ) )
10 8 9 syl 
 |-  ( E = { 0 , x } -> ( E e. ~P ( 0 ... N ) <-> E C_ ( 0 ... N ) ) )
11 10 a1i 
 |-  ( x e. ( 1 ... N ) -> ( E = { 0 , x } -> ( E e. ~P ( 0 ... N ) <-> E C_ ( 0 ... N ) ) ) )
12 11 rexlimiv 
 |-  ( E. x e. ( 1 ... N ) E = { 0 , x } -> ( E e. ~P ( 0 ... N ) <-> E C_ ( 0 ... N ) ) )
13 5 12 bianim 
 |-  ( E e. { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } <-> ( E C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) E = { 0 , x } ) )
14 2 13 bitrdi 
 |-  ( N e. NN0 -> ( E e. ( Edg ` ( StarGr ` N ) ) <-> ( E C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) E = { 0 , x } ) ) )