Theorem stgrusgra

Description: The star graph S_N is a simple graph. (Contributed by AV, 11-Sep-2025)

	Ref	Expression
Assertion	stgrusgra	Could not format assertion : No typesetting found for |- ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}}\right):\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\underset{1-1\; onto}{⟶}\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}$$
2		f1of1	$$⊢\left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}}\right):\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\underset{1-1\; onto}{⟶}\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\to \left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}}\right):\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\underset{1-1}{⟶}\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}$$
3	1 2	mp1i	$$⊢N\in {\mathbb{N}}_0\to \left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}}\right):\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\underset{1-1}{⟶}\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}$$
4		simpllr	$$⊢\left(\left(\left(N\in {\mathbb{N}}_0\wedge k\in 𝒫\left(0\dots N\right)\right)\wedge x\in \left(1\dots N\right)\right)\wedge k=\left\{0,x\right\}\right)\to k\in 𝒫\left(0\dots N\right)$$
5		fveq2	$$⊢k=\left\{0,x\right\}\to \left|k\right|=\left|\left\{0,x\right\}\right|$$
6		0red	$$⊢x\in \left(1\dots N\right)\to 0\in ℝ$$
7		elfznn	$$⊢x\in \left(1\dots N\right)\to x\in \mathbb{N}$$
8	7	nngt0d	$$⊢x\in \left(1\dots N\right)\to 0<x$$
9	6 8	ltned	$$⊢x\in \left(1\dots N\right)\to 0\ne x$$
10		c0ex	$$⊢0\in \mathrm{V}$$
11		vex	$$⊢x\in \mathrm{V}$$
12	10 11	pm3.2i	$$⊢\left(0\in \mathrm{V}\wedge x\in \mathrm{V}\right)$$
13		hashprg	$$⊢\left(0\in \mathrm{V}\wedge x\in \mathrm{V}\right)\to \left(0\ne x\leftrightarrow \left|\left\{0,x\right\}\right|=2\right)$$
14	12 13	mp1i	$$⊢x\in \left(1\dots N\right)\to \left(0\ne x\leftrightarrow \left|\left\{0,x\right\}\right|=2\right)$$
15	9 14	mpbid	$$⊢x\in \left(1\dots N\right)\to \left|\left\{0,x\right\}\right|=2$$
16	15	adantl	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge k\in 𝒫\left(0\dots N\right)\right)\wedge x\in \left(1\dots N\right)\right)\to \left|\left\{0,x\right\}\right|=2$$
17	5 16	sylan9eqr	$$⊢\left(\left(\left(N\in {\mathbb{N}}_0\wedge k\in 𝒫\left(0\dots N\right)\right)\wedge x\in \left(1\dots N\right)\right)\wedge k=\left\{0,x\right\}\right)\to \left|k\right|=2$$
18	4 17	jca	$$⊢\left(\left(\left(N\in {\mathbb{N}}_0\wedge k\in 𝒫\left(0\dots N\right)\right)\wedge x\in \left(1\dots N\right)\right)\wedge k=\left\{0,x\right\}\right)\to \left(k\in 𝒫\left(0\dots N\right)\wedge \left|k\right|=2\right)$$
19	18	ex	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge k\in 𝒫\left(0\dots N\right)\right)\wedge x\in \left(1\dots N\right)\right)\to \left(k=\left\{0,x\right\}\to \left(k\in 𝒫\left(0\dots N\right)\wedge \left|k\right|=2\right)\right)$$
20	19	rexlimdva	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in 𝒫\left(0\dots N\right)\right)\to \left(\exists x\in \left(1\dots N\right)k=\left\{0,x\right\}\to \left(k\in 𝒫\left(0\dots N\right)\wedge \left|k\right|=2\right)\right)$$
21	20	expimpd	$$⊢N\in {\mathbb{N}}_0\to \left(\left(k\in 𝒫\left(0\dots N\right)\wedge \exists x\in \left(1\dots N\right)k=\left\{0,x\right\}\right)\to \left(k\in 𝒫\left(0\dots N\right)\wedge \left|k\right|=2\right)\right)$$
22		eqeq1	$$⊢e=k\to \left(e=\left\{0,x\right\}\leftrightarrow k=\left\{0,x\right\}\right)$$
23	22	rexbidv	$$⊢e=k\to \left(\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\leftrightarrow \exists x\in \left(1\dots N\right)k=\left\{0,x\right\}\right)$$
24	23	elrab	$$⊢k\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(k\in 𝒫\left(0\dots N\right)\wedge \exists x\in \left(1\dots N\right)k=\left\{0,x\right\}\right)$$
25		fveqeq2	$$⊢e=k\to \left(\left|e\right|=2\leftrightarrow \left|k\right|=2\right)$$
26	25	elrab	$$⊢k\in \left\{e\in 𝒫\left(0\dots N\right)|\left|e\right|=2\right\}\leftrightarrow \left(k\in 𝒫\left(0\dots N\right)\wedge \left|k\right|=2\right)$$
27	21 24 26	3imtr4g	$$⊢N\in {\mathbb{N}}_0\to \left(k\in \left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\to k\in \left\{e\in 𝒫\left(0\dots N\right)|\left|e\right|=2\right\}\right)$$
28	27	ssrdv	$$⊢N\in {\mathbb{N}}_0\to \left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\subseteq \left\{e\in 𝒫\left(0\dots N\right)|\left|e\right|=2\right\}$$
29		f1ss	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}}\right):\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\underset{1-1}{⟶}\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\wedge \left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\subseteq \left\{e\in 𝒫\left(0\dots N\right)|\left|e\right|=2\right\}\right)\to \left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}}\right):\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\underset{1-1}{⟶}\left\{e\in 𝒫\left(0\dots N\right)|\left|e\right|=2\right\}$$
30	3 28 29	syl2anc	$$⊢N\in {\mathbb{N}}_0\to \left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}}\right):\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\underset{1-1}{⟶}\left\{e\in 𝒫\left(0\dots N\right)|\left|e\right|=2\right\}$$
31		stgriedg	Could not format ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) : No typesetting found for |- ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) with typecode |-
32	31	dmeqd	Could not format ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = dom ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) : No typesetting found for |- ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = dom ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) with typecode |-
33		dmresi	$$⊢\mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}}\right)=\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}$$
34	32 33	eqtrdi	Could not format ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : No typesetting found for |- ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) with typecode |-
35		stgrvtx	Could not format ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) : No typesetting found for |- ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) with typecode |-
36	35	pweqd	Could not format ( N e. NN0 -> ~P ( Vtx ` ( StarGr ` N ) ) = ~P ( 0 ... N ) ) : No typesetting found for |- ( N e. NN0 -> ~P ( Vtx ` ( StarGr ` N ) ) = ~P ( 0 ... N ) ) with typecode |-
37	36	rabeqdv	Could not format ( N e. NN0 -> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } = { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) : No typesetting found for |- ( N e. NN0 -> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } = { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) with typecode |-
38	31 34 37	f1eq123d	Could not format ( N e. NN0 -> ( ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } <-> ( _I |` { 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 } } -1-1-> { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) ) : No typesetting found for |- ( N e. NN0 -> ( ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } <-> ( _I |` { 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 } } -1-1-> { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) ) with typecode |-
39	30 38	mpbird	Could not format ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) : No typesetting found for |- ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) with typecode |-
40		fvex	Could not format ( StarGr ` N ) e. _V : No typesetting found for |- ( StarGr ` N ) e. _V with typecode |-
41		eqid	Could not format ( Vtx ` ( StarGr ` N ) ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- ( Vtx ` ( StarGr ` N ) ) = ( Vtx ` ( StarGr ` N ) ) with typecode |-
42		eqid	Could not format ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` ( StarGr ` N ) ) : No typesetting found for |- ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` ( StarGr ` N ) ) with typecode |-
43	41 42	isusgrs	Could not format ( ( StarGr ` N ) e. _V -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) : No typesetting found for |- ( ( StarGr ` N ) e. _V -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) with typecode |-
44	40 43	mp1i	Could not format ( N e. NN0 -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) : No typesetting found for |- ( N e. NN0 -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) with typecode |-
45	39 44	mpbird	Could not format ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) : No typesetting found for |- ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) with typecode |-