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		0elpr01	$$⊢0\in \left\{0,1\right\}$$
18	17 4	eleqtrri	$$⊢0\in \left(0\dots 1\right)$$
19		1ex	$$⊢1\in \mathrm{V}$$
20	19	prid2	$$⊢1\in \left\{0,1\right\}$$
21	20 4	eleqtrri	$$⊢1\in \left(0\dots 1\right)$$
22		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)$$
23	18 21 22	mp2an	$$⊢\left\{0,1\right\}\in 𝒫\left(0\dots 1\right)$$
24		eqid	$$⊢\left\{0,1\right\}=\left\{0,1\right\}$$
25	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\}$$
26	7	eqeq2d	$$⊢x=1\to \left(\left\{0,1\right\}=\left\{0,x\right\}\leftrightarrow \left\{0,1\right\}=\left\{0,1\right\}\right)$$
27	19 26	rexsn	$$⊢\exists x\in \left\{1\right\}\left\{0,1\right\}=\left\{0,x\right\}\leftrightarrow \left\{0,1\right\}=\left\{0,1\right\}$$
28	25 27	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\}$$
29	24 28	mpbir	$$⊢\exists x\in \left(1\dots 1\right)\left\{0,1\right\}=\left\{0,x\right\}$$
30	23 29	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)$$
31		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)$$
32		eqeq1	$$⊢e=\left\{0,1\right\}\to \left(e=\left\{0,x\right\}\leftrightarrow \left\{0,1\right\}=\left\{0,x\right\}\right)$$
33	32	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)$$
34	31 33	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)$$
35	30 34	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)$$
36	16 35	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\}$$
37	36	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\}$$
38		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\}$$
39		df-sn	$$⊢\left\{\left\{0,1\right\}\right\}=\left\{e|e=\left\{0,1\right\}\right\}$$
40	37 38 39	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\}$$
41	40	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\}}$$
42	41	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\}}⟩$$
43	5 42	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\}$$
44	3 43	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 |-