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\in \bigcup _{x=1}^N\left\{\left\{0,x\right\}\right\}\leftrightarrow \exists x\in \left(1\dots N\right)e\in \left\{\left\{0,x\right\}\right\}$$
3	2	a1i	$$⊢N\in {\mathbb{N}}_0\to \left(e\in \bigcup _{x=1}^N\left\{\left\{0,x\right\}\right\}\leftrightarrow \exists x\in \left(1\dots N\right)e\in \left\{\left\{0,x\right\}\right\}\right)$$
4		velsn	$$⊢e\in \left\{\left\{0,x\right\}\right\}\leftrightarrow e=\left\{0,x\right\}$$
5		0elfz	$$⊢N\in {\mathbb{N}}_0\to 0\in \left(0\dots N\right)$$
6	5	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(1\dots N\right)\right)\to 0\in \left(0\dots N\right)$$
7		fz1ssfz0	$$⊢\left(1\dots N\right)\subseteq \left(0\dots N\right)$$
8	7	sseli	$$⊢x\in \left(1\dots N\right)\to x\in \left(0\dots N\right)$$
9	8	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(1\dots N\right)\right)\to x\in \left(0\dots N\right)$$
10	6 9	prssd	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(1\dots N\right)\right)\to \left\{0,x\right\}\subseteq \left(0\dots N\right)$$
11		sseq1	$$⊢e=\left\{0,x\right\}\to \left(e\subseteq \left(0\dots N\right)\leftrightarrow \left\{0,x\right\}\subseteq \left(0\dots N\right)\right)$$
12	10 11	syl5ibrcom	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(1\dots N\right)\right)\to \left(e=\left\{0,x\right\}\to e\subseteq \left(0\dots N\right)\right)$$
13	12	pm4.71rd	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(1\dots N\right)\right)\to \left(e=\left\{0,x\right\}\leftrightarrow \left(e\subseteq \left(0\dots N\right)\wedge e=\left\{0,x\right\}\right)\right)$$
14	4 13	bitr2id	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \left(1\dots N\right)\right)\to \left(\left(e\subseteq \left(0\dots N\right)\wedge e=\left\{0,x\right\}\right)\leftrightarrow e\in \left\{\left\{0,x\right\}\right\}\right)$$
15	14	rexbidva	$$⊢N\in {\mathbb{N}}_0\to \left(\exists x\in \left(1\dots N\right)\left(e\subseteq \left(0\dots N\right)\wedge e=\left\{0,x\right\}\right)\leftrightarrow \exists x\in \left(1\dots N\right)e\in \left\{\left\{0,x\right\}\right\}\right)$$
16		r19.42v	$$⊢\exists x\in \left(1\dots N\right)\left(e\subseteq \left(0\dots N\right)\wedge 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)$$
17	16	a1i	$$⊢N\in {\mathbb{N}}_0\to \left(\exists x\in \left(1\dots N\right)\left(e\subseteq \left(0\dots N\right)\wedge 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)\right)$$
18	3 15 17	3bitr2rd	$$⊢N\in {\mathbb{N}}_0\to \left(\left(e\subseteq \left(0\dots N\right)\wedge \exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right)\leftrightarrow e\in \bigcup _{x=1}^N\left\{\left\{0,x\right\}\right\}\right)$$
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 |-