Theorem ex-chn2

Description: Example: sequence <" ZZ NN QQ "> is a valid chain under the equinumerosity relation in universal domain. (Contributed by Ender Ting, 17-Jan-2026)

	Ref	Expression
Assertion	ex-chn2	$$⊢⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\approx$$

Proof

Step	Hyp	Ref	Expression
1		s3cli	$$⊢⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\in \mathrm{Word}\mathrm{V}$$
2		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
3		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
4		qex	$$⊢\mathbb{Q}\in \mathrm{V}$$
5		s3fn	$$⊢\left(\mathbb{Z}\in \mathrm{V}\wedge \mathbb{N}\in \mathrm{V}\wedge \mathbb{Q}\in \mathrm{V}\right)\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩Fn\left\{0,1,2\right\}$$
6	2 3 4 5	mp3an	$$⊢⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩Fn\left\{0,1,2\right\}$$
7	6	fndmi	$$⊢\mathrm{dom}⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩=\left\{0,1,2\right\}$$
8	7	difeq1i	$$⊢\mathrm{dom}⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\setminus \left\{0\right\}=\left\{0,1,2\right\}\setminus \left\{0\right\}$$
9		tprot	$$⊢\left\{0,1,2\right\}=\left\{1,2,0\right\}$$
10	9	difeq1i	$$⊢\left\{0,1,2\right\}\setminus \left\{0\right\}=\left\{1,2,0\right\}\setminus \left\{0\right\}$$
11		ax-1ne0	$$⊢1\ne 0$$
12		2ne0	$$⊢2\ne 0$$
13		diftpsn3	$$⊢\left(1\ne 0\wedge 2\ne 0\right)\to \left\{1,2,0\right\}\setminus \left\{0\right\}=\left\{1,2\right\}$$
14	11 12 13	mp2an	$$⊢\left\{1,2,0\right\}\setminus \left\{0\right\}=\left\{1,2\right\}$$
15	8 10 14	3eqtri	$$⊢\mathrm{dom}⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\setminus \left\{0\right\}=\left\{1,2\right\}$$
16	15	eleq2i	$$⊢x\in \left(\mathrm{dom}⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\setminus \left\{0\right\}\right)\leftrightarrow x\in \left\{1,2\right\}$$
17	16	biimpi	$$⊢x\in \left(\mathrm{dom}⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\setminus \left\{0\right\}\right)\to x\in \left\{1,2\right\}$$
18		elpri	$$⊢x\in \left\{1,2\right\}\to \left(x=1\vee x=2\right)$$
19		znnen	$$⊢\mathbb{Z}\approx \mathbb{N}$$
20	19	a1i	$$⊢x=1\to \mathbb{Z}\approx \mathbb{N}$$
21		oveq1	$$⊢x=1\to x-1=1-1$$
22		1m1e0	$$⊢1-1=0$$
23	21 22	eqtrdi	$$⊢x=1\to x-1=0$$
24	23	fveq2d	$$⊢x=1\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x-1\right)=⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(0\right)$$
25		s3fv0	$$⊢\mathbb{Z}\in \mathrm{V}\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(0\right)=\mathbb{Z}$$
26	2 25	ax-mp	$$⊢⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(0\right)=\mathbb{Z}$$
27	24 26	eqtrdi	$$⊢x=1\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x-1\right)=\mathbb{Z}$$
28		fveq2	$$⊢x=1\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x\right)=⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(1\right)$$
29		s3fv1	$$⊢\mathbb{N}\in \mathrm{V}\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(1\right)=\mathbb{N}$$
30	3 29	ax-mp	$$⊢⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(1\right)=\mathbb{N}$$
31	28 30	eqtrdi	$$⊢x=1\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x\right)=\mathbb{N}$$
32	20 27 31	3brtr4d	$$⊢x=1\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x-1\right)\approx ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x\right)$$
33		qnnen	$$⊢\mathbb{Q}\approx \mathbb{N}$$
34	33	ensymi	$$⊢\mathbb{N}\approx \mathbb{Q}$$
35	34	a1i	$$⊢x=2\to \mathbb{N}\approx \mathbb{Q}$$
36		oveq1	$$⊢x=2\to x-1=2-1$$
37		2m1e1	$$⊢2-1=1$$
38	36 37	eqtrdi	$$⊢x=2\to x-1=1$$
39	38	fveq2d	$$⊢x=2\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x-1\right)=⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(1\right)$$
40	39 30	eqtrdi	$$⊢x=2\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x-1\right)=\mathbb{N}$$
41		fveq2	$$⊢x=2\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x\right)=⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(2\right)$$
42		s3fv2	$$⊢\mathbb{Q}\in \mathrm{V}\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(2\right)=\mathbb{Q}$$
43	4 42	ax-mp	$$⊢⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(2\right)=\mathbb{Q}$$
44	41 43	eqtrdi	$$⊢x=2\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x\right)=\mathbb{Q}$$
45	35 40 44	3brtr4d	$$⊢x=2\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x-1\right)\approx ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x\right)$$
46	32 45	jaoi	$$⊢\left(x=1\vee x=2\right)\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x-1\right)\approx ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x\right)$$
47	17 18 46	3syl	$$⊢x\in \left(\mathrm{dom}⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\setminus \left\{0\right\}\right)\to ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x-1\right)\approx ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x\right)$$
48	47	rgen	$$⊢\forall x\in \left(\mathrm{dom}⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\setminus \left\{0\right\}\right)⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x-1\right)\approx ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x\right)$$
49		ischn	$$⊢⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\approx \leftrightarrow \left(⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\in \mathrm{Word}\mathrm{V}\wedge \forall x\in \left(\mathrm{dom}⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\setminus \left\{0\right\}\right)⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x-1\right)\approx ⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\left(x\right)\right)$$
50	1 48 49	mpbir2an	$$⊢⟨“\mathbb{Z}\mathbb{N}\mathbb{Q}”⟩\in {\mathrm{Chain}}_{\mathrm{V}}\approx$$