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	⊢ ⟨“ ℤ ℕ ℚ ”⟩ ∈ ( ≈ Chain V )

Proof

Step	Hyp	Ref	Expression
1		s3cli	⊢ ⟨“ ℤ ℕ ℚ ”⟩ ∈ Word V
2		zex	⊢ ℤ ∈ V
3		nnex	⊢ ℕ ∈ V
4		qex	⊢ ℚ ∈ V
5		s3fn	⊢ ( ( ℤ ∈ V ∧ ℕ ∈ V ∧ ℚ ∈ V ) → ⟨“ ℤ ℕ ℚ ”⟩ Fn { 0 , 1 , 2 } )
6	2 3 4 5	mp3an	⊢ ⟨“ ℤ ℕ ℚ ”⟩ Fn { 0 , 1 , 2 }
7	6	fndmi	⊢ dom ⟨“ ℤ ℕ ℚ ”⟩ = { 0 , 1 , 2 }
8	7	difeq1i	⊢ ( dom ⟨“ ℤ ℕ ℚ ”⟩ ∖ { 0 } ) = ( { 0 , 1 , 2 } ∖ { 0 } )
9		tprot	⊢ { 0 , 1 , 2 } = { 1 , 2 , 0 }
10	9	difeq1i	⊢ ( { 0 , 1 , 2 } ∖ { 0 } ) = ( { 1 , 2 , 0 } ∖ { 0 } )
11		ax-1ne0	⊢ 1 ≠ 0
12		2ne0	⊢ 2 ≠ 0
13		diftpsn3	⊢ ( ( 1 ≠ 0 ∧ 2 ≠ 0 ) → ( { 1 , 2 , 0 } ∖ { 0 } ) = { 1 , 2 } )
14	11 12 13	mp2an	⊢ ( { 1 , 2 , 0 } ∖ { 0 } ) = { 1 , 2 }
15	8 10 14	3eqtri	⊢ ( dom ⟨“ ℤ ℕ ℚ ”⟩ ∖ { 0 } ) = { 1 , 2 }
16	15	eleq2i	⊢ ( 𝑥 ∈ ( dom ⟨“ ℤ ℕ ℚ ”⟩ ∖ { 0 } ) ↔ 𝑥 ∈ { 1 , 2 } )
17	16	biimpi	⊢ ( 𝑥 ∈ ( dom ⟨“ ℤ ℕ ℚ ”⟩ ∖ { 0 } ) → 𝑥 ∈ { 1 , 2 } )
18		elpri	⊢ ( 𝑥 ∈ { 1 , 2 } → ( 𝑥 = 1 ∨ 𝑥 = 2 ) )
19		znnen	⊢ ℤ ≈ ℕ
20	19	a1i	⊢ ( 𝑥 = 1 → ℤ ≈ ℕ )
21		oveq1	⊢ ( 𝑥 = 1 → ( 𝑥 − 1 ) = ( 1 − 1 ) )
22		1m1e0	⊢ ( 1 − 1 ) = 0
23	21 22	eqtrdi	⊢ ( 𝑥 = 1 → ( 𝑥 − 1 ) = 0 )
24	23	fveq2d	⊢ ( 𝑥 = 1 → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ ( 𝑥 − 1 ) ) = ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 0 ) )
25		s3fv0	⊢ ( ℤ ∈ V → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 0 ) = ℤ )
26	2 25	ax-mp	⊢ ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 0 ) = ℤ
27	24 26	eqtrdi	⊢ ( 𝑥 = 1 → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ ( 𝑥 − 1 ) ) = ℤ )
28		fveq2	⊢ ( 𝑥 = 1 → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 𝑥 ) = ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 1 ) )
29		s3fv1	⊢ ( ℕ ∈ V → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 1 ) = ℕ )
30	3 29	ax-mp	⊢ ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 1 ) = ℕ
31	28 30	eqtrdi	⊢ ( 𝑥 = 1 → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 𝑥 ) = ℕ )
32	20 27 31	3brtr4d	⊢ ( 𝑥 = 1 → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ ( 𝑥 − 1 ) ) ≈ ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 𝑥 ) )
33		qnnen	⊢ ℚ ≈ ℕ
34	33	ensymi	⊢ ℕ ≈ ℚ
35	34	a1i	⊢ ( 𝑥 = 2 → ℕ ≈ ℚ )
36		oveq1	⊢ ( 𝑥 = 2 → ( 𝑥 − 1 ) = ( 2 − 1 ) )
37		2m1e1	⊢ ( 2 − 1 ) = 1
38	36 37	eqtrdi	⊢ ( 𝑥 = 2 → ( 𝑥 − 1 ) = 1 )
39	38	fveq2d	⊢ ( 𝑥 = 2 → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ ( 𝑥 − 1 ) ) = ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 1 ) )
40	39 30	eqtrdi	⊢ ( 𝑥 = 2 → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ ( 𝑥 − 1 ) ) = ℕ )
41		fveq2	⊢ ( 𝑥 = 2 → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 𝑥 ) = ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 2 ) )
42		s3fv2	⊢ ( ℚ ∈ V → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 2 ) = ℚ )
43	4 42	ax-mp	⊢ ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 2 ) = ℚ
44	41 43	eqtrdi	⊢ ( 𝑥 = 2 → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 𝑥 ) = ℚ )
45	35 40 44	3brtr4d	⊢ ( 𝑥 = 2 → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ ( 𝑥 − 1 ) ) ≈ ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 𝑥 ) )
46	32 45	jaoi	⊢ ( ( 𝑥 = 1 ∨ 𝑥 = 2 ) → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ ( 𝑥 − 1 ) ) ≈ ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 𝑥 ) )
47	17 18 46	3syl	⊢ ( 𝑥 ∈ ( dom ⟨“ ℤ ℕ ℚ ”⟩ ∖ { 0 } ) → ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ ( 𝑥 − 1 ) ) ≈ ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 𝑥 ) )
48	47	rgen	⊢ ∀ 𝑥 ∈ ( dom ⟨“ ℤ ℕ ℚ ”⟩ ∖ { 0 } ) ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ ( 𝑥 − 1 ) ) ≈ ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 𝑥 )
49		ischn	⊢ ( ⟨“ ℤ ℕ ℚ ”⟩ ∈ ( ≈ Chain V ) ↔ ( ⟨“ ℤ ℕ ℚ ”⟩ ∈ Word V ∧ ∀ 𝑥 ∈ ( dom ⟨“ ℤ ℕ ℚ ”⟩ ∖ { 0 } ) ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ ( 𝑥 − 1 ) ) ≈ ( ⟨“ ℤ ℕ ℚ ”⟩ ‘ 𝑥 ) ) )
50	1 48 49	mpbir2an	⊢ ⟨“ ℤ ℕ ℚ ”⟩ ∈ ( ≈ Chain V )