Theorem ex-chn1

Description: Example: a doubleton of twos is a valid chain under the identity relation and domain of integers. (Contributed by Ender Ting, 17-Jan-2026)

	Ref	Expression
Assertion	ex-chn1	$$⊢⟨“22”⟩\in {\mathrm{Chain}}_{\mathbb{Z}}\mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		2z	$$⊢2\in \mathbb{Z}$$
2		s2cl	$$⊢\left(2\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to ⟨“22”⟩\in \mathrm{Word}\mathbb{Z}$$
3	1 1 2	mp2an	$$⊢⟨“22”⟩\in \mathrm{Word}\mathbb{Z}$$
4		s2dm	$$⊢\mathrm{dom}⟨“22”⟩=\left\{0,1\right\}$$
5	4	difeq1i	$$⊢\mathrm{dom}⟨“22”⟩\setminus \left\{0\right\}=\left\{0,1\right\}\setminus \left\{0\right\}$$
6	5	eleq2i	$$⊢x\in \left(\mathrm{dom}⟨“22”⟩\setminus \left\{0\right\}\right)\leftrightarrow x\in \left(\left\{0,1\right\}\setminus \left\{0\right\}\right)$$
7	6	biimpi	$$⊢x\in \left(\mathrm{dom}⟨“22”⟩\setminus \left\{0\right\}\right)\to x\in \left(\left\{0,1\right\}\setminus \left\{0\right\}\right)$$
8		difprsnss	$$⊢\left\{0,1\right\}\setminus \left\{0\right\}\subseteq \left\{1\right\}$$
9	8	sseli	$$⊢x\in \left(\left\{0,1\right\}\setminus \left\{0\right\}\right)\to x\in \left\{1\right\}$$
10	9	elsnd	$$⊢x\in \left(\left\{0,1\right\}\setminus \left\{0\right\}\right)\to x=1$$
11		eqid	$$⊢2=2$$
12		2ex	$$⊢2\in \mathrm{V}$$
13	12	ideq	$$⊢2\mathrm{I}2\leftrightarrow 2=2$$
14	11 13	mpbir	$$⊢2\mathrm{I}2$$
15	14	a1i	$$⊢x=1\to 2\mathrm{I}2$$
16		oveq1	$$⊢x=1\to x-1=1-1$$
17		1m1e0	$$⊢1-1=0$$
18	16 17	eqtrdi	$$⊢x=1\to x-1=0$$
19		fveq2	$$⊢x-1=0\to ⟨“22”⟩\left(x-1\right)=⟨“22”⟩\left(0\right)$$
20		s2fv0	$$⊢2\in \mathrm{V}\to ⟨“22”⟩\left(0\right)=2$$
21	12 20	ax-mp	$$⊢⟨“22”⟩\left(0\right)=2$$
22	19 21	eqtr2di	$$⊢x-1=0\to 2=⟨“22”⟩\left(x-1\right)$$
23	18 22	syl	$$⊢x=1\to 2=⟨“22”⟩\left(x-1\right)$$
24		fveq2	$$⊢x=1\to ⟨“22”⟩\left(x\right)=⟨“22”⟩\left(1\right)$$
25		s2fv1	$$⊢2\in \mathrm{V}\to ⟨“22”⟩\left(1\right)=2$$
26	12 25	ax-mp	$$⊢⟨“22”⟩\left(1\right)=2$$
27	24 26	eqtr2di	$$⊢x=1\to 2=⟨“22”⟩\left(x\right)$$
28	15 23 27	3brtr3d	$$⊢x=1\to ⟨“22”⟩\left(x-1\right)\mathrm{I}⟨“22”⟩\left(x\right)$$
29	7 10 28	3syl	$$⊢x\in \left(\mathrm{dom}⟨“22”⟩\setminus \left\{0\right\}\right)\to ⟨“22”⟩\left(x-1\right)\mathrm{I}⟨“22”⟩\left(x\right)$$
30	29	rgen	$$⊢\forall x\in \left(\mathrm{dom}⟨“22”⟩\setminus \left\{0\right\}\right)⟨“22”⟩\left(x-1\right)\mathrm{I}⟨“22”⟩\left(x\right)$$
31		ischn	$$⊢⟨“22”⟩\in {\mathrm{Chain}}_{\mathbb{Z}}\mathrm{I}\leftrightarrow \left(⟨“22”⟩\in \mathrm{Word}\mathbb{Z}\wedge \forall x\in \left(\mathrm{dom}⟨“22”⟩\setminus \left\{0\right\}\right)⟨“22”⟩\left(x-1\right)\mathrm{I}⟨“22”⟩\left(x\right)\right)$$
32	3 30 31	mpbir2an	$$⊢⟨“22”⟩\in {\mathrm{Chain}}_{\mathbb{Z}}\mathrm{I}$$