Theorem stgr1

Description: The star graph S_1 consists of a single simple edge. (Contributed by AV, 11-Sep-2025)

	Ref	Expression
Assertion	stgr1	Could not format assertion : No typesetting found for |- ( StarGr ` 1 ) = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( .ef ` ndx ) , ( _I |` { { 0 , 1 } } ) >. } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		stgrfv	Could not format ( 1 e. NN0 -> ( StarGr ` 1 ) = { <. ( Base ` ndx ) , ( 0 ... 1 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 1 ) | E. x e. ( 1 ... 1 ) e = { 0 , x } } ) >. } ) : No typesetting found for |- ( 1 e. NN0 -> ( StarGr ` 1 ) = { <. ( Base ` ndx ) , ( 0 ... 1 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 1 ) | E. x e. ( 1 ... 1 ) e = { 0 , x } } ) >. } ) with typecode |-
3	1 2	ax-mp	Could not format ( StarGr ` 1 ) = { <. ( Base ` ndx ) , ( 0 ... 1 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 1 ) | E. x e. ( 1 ... 1 ) e = { 0 , x } } ) >. } : No typesetting found for |- ( StarGr ` 1 ) = { <. ( Base ` ndx ) , ( 0 ... 1 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 1 ) | E. x e. ( 1 ... 1 ) e = { 0 , x } } ) >. } with typecode |-
4		fz01pr	$$⊢\left(0\dots 1\right)=\left\{0,1\right\}$$
5	4	opeq2i	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(0\dots 1\right)⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩$$
6		elsni	$$⊢x\in \left\{1\right\}\to x=1$$
7		preq2	$$⊢x=1\to \left\{0,x\right\}=\left\{0,1\right\}$$
8	7	eqeq2d	$$⊢x=1\to \left(e=\left\{0,x\right\}\leftrightarrow e=\left\{0,1\right\}\right)$$
9	8	biimpd	$$⊢x=1\to \left(e=\left\{0,x\right\}\to e=\left\{0,1\right\}\right)$$
10	6 9	syl	$$⊢x\in \left\{1\right\}\to \left(e=\left\{0,x\right\}\to e=\left\{0,1\right\}\right)$$
11		1z	$$⊢1\in \mathbb{Z}$$
12		fzsn	$$⊢1\in \mathbb{Z}\to \left(1\dots 1\right)=\left\{1\right\}$$
13	11 12	ax-mp	$$⊢\left(1\dots 1\right)=\left\{1\right\}$$
14	10 13	eleq2s	$$⊢x\in \left(1\dots 1\right)\to \left(e=\left\{0,x\right\}\to e=\left\{0,1\right\}\right)$$
15	14	rexlimiv	$$⊢\exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\to e=\left\{0,1\right\}$$
16	15	adantl	$$⊢\left(e\in 𝒫\left(0\dots 1\right)\wedge \exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\right)\to e=\left\{0,1\right\}$$
17		c0ex	$$⊢0\in \mathrm{V}$$
18	17	prid1	$$⊢0\in \left\{0,1\right\}$$
19	18 4	eleqtrri	$$⊢0\in \left(0\dots 1\right)$$
20		1ex	$$⊢1\in \mathrm{V}$$
21	20	prid2	$$⊢1\in \left\{0,1\right\}$$
22	21 4	eleqtrri	$$⊢1\in \left(0\dots 1\right)$$
23		prelpwi	$$⊢\left(0\in \left(0\dots 1\right)\wedge 1\in \left(0\dots 1\right)\right)\to \left\{0,1\right\}\in 𝒫\left(0\dots 1\right)$$
24	19 22 23	mp2an	$$⊢\left\{0,1\right\}\in 𝒫\left(0\dots 1\right)$$
25		eqid	$$⊢\left\{0,1\right\}=\left\{0,1\right\}$$
26	13	rexeqi	$$⊢\exists x\in \left(1\dots 1\right)\left\{0,1\right\}=\left\{0,x\right\}\leftrightarrow \exists x\in \left\{1\right\}\left\{0,1\right\}=\left\{0,x\right\}$$
27	7	eqeq2d	$$⊢x=1\to \left(\left\{0,1\right\}=\left\{0,x\right\}\leftrightarrow \left\{0,1\right\}=\left\{0,1\right\}\right)$$
28	20 27	rexsn	$$⊢\exists x\in \left\{1\right\}\left\{0,1\right\}=\left\{0,x\right\}\leftrightarrow \left\{0,1\right\}=\left\{0,1\right\}$$
29	26 28	bitri	$$⊢\exists x\in \left(1\dots 1\right)\left\{0,1\right\}=\left\{0,x\right\}\leftrightarrow \left\{0,1\right\}=\left\{0,1\right\}$$
30	25 29	mpbir	$$⊢\exists x\in \left(1\dots 1\right)\left\{0,1\right\}=\left\{0,x\right\}$$
31	24 30	pm3.2i	$$⊢\left(\left\{0,1\right\}\in 𝒫\left(0\dots 1\right)\wedge \exists x\in \left(1\dots 1\right)\left\{0,1\right\}=\left\{0,x\right\}\right)$$
32		eleq1	$$⊢e=\left\{0,1\right\}\to \left(e\in 𝒫\left(0\dots 1\right)\leftrightarrow \left\{0,1\right\}\in 𝒫\left(0\dots 1\right)\right)$$
33		eqeq1	$$⊢e=\left\{0,1\right\}\to \left(e=\left\{0,x\right\}\leftrightarrow \left\{0,1\right\}=\left\{0,x\right\}\right)$$
34	33	rexbidv	$$⊢e=\left\{0,1\right\}\to \left(\exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\leftrightarrow \exists x\in \left(1\dots 1\right)\left\{0,1\right\}=\left\{0,x\right\}\right)$$
35	32 34	anbi12d	$$⊢e=\left\{0,1\right\}\to \left(\left(e\in 𝒫\left(0\dots 1\right)\wedge \exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\right)\leftrightarrow \left(\left\{0,1\right\}\in 𝒫\left(0\dots 1\right)\wedge \exists x\in \left(1\dots 1\right)\left\{0,1\right\}=\left\{0,x\right\}\right)\right)$$
36	31 35	mpbiri	$$⊢e=\left\{0,1\right\}\to \left(e\in 𝒫\left(0\dots 1\right)\wedge \exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\right)$$
37	16 36	impbii	$$⊢\left(e\in 𝒫\left(0\dots 1\right)\wedge \exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\right)\leftrightarrow e=\left\{0,1\right\}$$
38	37	abbii	$$⊢\left\{e|\left(e\in 𝒫\left(0\dots 1\right)\wedge \exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\right)\right\}=\left\{e|e=\left\{0,1\right\}\right\}$$
39		df-rab	$$⊢\left\{e\in 𝒫\left(0\dots 1\right)|\exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\right\}=\left\{e|\left(e\in 𝒫\left(0\dots 1\right)\wedge \exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\right)\right\}$$
40		df-sn	$$⊢\left\{\left\{0,1\right\}\right\}=\left\{e|e=\left\{0,1\right\}\right\}$$
41	38 39 40	3eqtr4i	$$⊢\left\{e\in 𝒫\left(0\dots 1\right)|\exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\right\}=\left\{\left\{0,1\right\}\right\}$$
42	41	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots 1\right)|\exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\right\}}={\mathrm{I}\upharpoonright }_{\left\{\left\{0,1\right\}\right\}}$$
43	42	opeq2i	$$⊢⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots 1\right)|\exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\right\}}⟩=⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{\left\{0,1\right\}\right\}}⟩$$
44	5 43	preq12i	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(0\dots 1\right)⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots 1\right)|\exists x\in \left(1\dots 1\right)e=\left\{0,x\right\}\right\}}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{\left\{0,1\right\}\right\}}⟩\right\}$$
45	3 44	eqtri	Could not format ( StarGr ` 1 ) = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( .ef ` ndx ) , ( _I |` { { 0 , 1 } } ) >. } : No typesetting found for |- ( StarGr ` 1 ) = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( .ef ` ndx ) , ( _I |` { { 0 , 1 } } ) >. } with typecode |-