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\to \left(e=\left\{0,x\right\}\leftrightarrow E=\left\{0,x\right\}\right)$$
4	3	rexbidv	$$⊢e=E\to \left(\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\leftrightarrow \exists x\in \left(1\dots N\right)E=\left\{0,x\right\}\right)$$
5	4	elrab	$$⊢E\in \left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\leftrightarrow \left(E\in 𝒫\left(0\dots N\right)\wedge \exists x\in \left(1\dots N\right)E=\left\{0,x\right\}\right)$$
6		prex	$$⊢\left\{0,x\right\}\in \mathrm{V}$$
7		eleq1	$$⊢E=\left\{0,x\right\}\to \left(E\in \mathrm{V}\leftrightarrow \left\{0,x\right\}\in \mathrm{V}\right)$$
8	6 7	mpbiri	$$⊢E=\left\{0,x\right\}\to E\in \mathrm{V}$$
9		elpwg	$$⊢E\in \mathrm{V}\to \left(E\in 𝒫\left(0\dots N\right)\leftrightarrow E\subseteq \left(0\dots N\right)\right)$$
10	8 9	syl	$$⊢E=\left\{0,x\right\}\to \left(E\in 𝒫\left(0\dots N\right)\leftrightarrow E\subseteq \left(0\dots N\right)\right)$$
11	10	a1i	$$⊢x\in \left(1\dots N\right)\to \left(E=\left\{0,x\right\}\to \left(E\in 𝒫\left(0\dots N\right)\leftrightarrow E\subseteq \left(0\dots N\right)\right)\right)$$
12	11	rexlimiv	$$⊢\exists x\in \left(1\dots N\right)E=\left\{0,x\right\}\to \left(E\in 𝒫\left(0\dots N\right)\leftrightarrow E\subseteq \left(0\dots N\right)\right)$$
13	5 12	bianim	$$⊢E\in \left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\leftrightarrow \left(E\subseteq \left(0\dots N\right)\wedge \exists x\in \left(1\dots N\right)E=\left\{0,x\right\}\right)$$
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 |-