Metamath Proof Explorer


Theorem stgredgel

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

Ref Expression
Assertion stgredgel Could not format assertion : 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 |-

Proof

Step Hyp Ref Expression
1 stgredg Could not format ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : No typesetting found for |- ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) with typecode |-
2 1 eleq2d Could not format ( N e. NN0 -> ( E e. ( Edg ` ( StarGr ` N ) ) <-> E e. { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) : No typesetting found for |- ( N e. NN0 -> ( E e. ( Edg ` ( StarGr ` N ) ) <-> E e. { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) with typecode |-
3 eqeq1 e = E e = 0 x E = 0 x
4 3 rexbidv e = E x 1 N e = 0 x x 1 N E = 0 x
5 4 elrab E e 𝒫 0 N | x 1 N e = 0 x E 𝒫 0 N x 1 N E = 0 x
6 prex 0 x V
7 eleq1 E = 0 x E V 0 x V
8 6 7 mpbiri E = 0 x E V
9 elpwg E V E 𝒫 0 N E 0 N
10 8 9 syl E = 0 x E 𝒫 0 N E 0 N
11 10 a1i x 1 N E = 0 x E 𝒫 0 N E 0 N
12 11 rexlimiv x 1 N E = 0 x E 𝒫 0 N E 0 N
13 5 12 bianim E e 𝒫 0 N | x 1 N e = 0 x E 0 N x 1 N E = 0 x
14 2 13 bitrdi 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 |-