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	⊢ ⟨“ 2 2 ”⟩ ∈ ( I Chain ℤ )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		s2cl	⊢ ( ( 2 ∈ ℤ ∧ 2 ∈ ℤ ) → ⟨“ 2 2 ”⟩ ∈ Word ℤ )
3	1 1 2	mp2an	⊢ ⟨“ 2 2 ”⟩ ∈ Word ℤ
4		s2dm	⊢ dom ⟨“ 2 2 ”⟩ = { 0 , 1 }
5	4	difeq1i	⊢ ( dom ⟨“ 2 2 ”⟩ ∖ { 0 } ) = ( { 0 , 1 } ∖ { 0 } )
6	5	eleq2i	⊢ ( 𝑥 ∈ ( dom ⟨“ 2 2 ”⟩ ∖ { 0 } ) ↔ 𝑥 ∈ ( { 0 , 1 } ∖ { 0 } ) )
7	6	biimpi	⊢ ( 𝑥 ∈ ( dom ⟨“ 2 2 ”⟩ ∖ { 0 } ) → 𝑥 ∈ ( { 0 , 1 } ∖ { 0 } ) )
8		difprsnss	⊢ ( { 0 , 1 } ∖ { 0 } ) ⊆ { 1 }
9	8	sseli	⊢ ( 𝑥 ∈ ( { 0 , 1 } ∖ { 0 } ) → 𝑥 ∈ { 1 } )
10	9	elsnd	⊢ ( 𝑥 ∈ ( { 0 , 1 } ∖ { 0 } ) → 𝑥 = 1 )
11		eqid	⊢ 2 = 2
12		2ex	⊢ 2 ∈ V
13	12	ideq	⊢ ( 2 I 2 ↔ 2 = 2 )
14	11 13	mpbir	⊢ 2 I 2
15	14	a1i	⊢ ( 𝑥 = 1 → 2 I 2 )
16		oveq1	⊢ ( 𝑥 = 1 → ( 𝑥 − 1 ) = ( 1 − 1 ) )
17		1m1e0	⊢ ( 1 − 1 ) = 0
18	16 17	eqtrdi	⊢ ( 𝑥 = 1 → ( 𝑥 − 1 ) = 0 )
19		fveq2	⊢ ( ( 𝑥 − 1 ) = 0 → ( ⟨“ 2 2 ”⟩ ‘ ( 𝑥 − 1 ) ) = ( ⟨“ 2 2 ”⟩ ‘ 0 ) )
20		s2fv0	⊢ ( 2 ∈ V → ( ⟨“ 2 2 ”⟩ ‘ 0 ) = 2 )
21	12 20	ax-mp	⊢ ( ⟨“ 2 2 ”⟩ ‘ 0 ) = 2
22	19 21	eqtr2di	⊢ ( ( 𝑥 − 1 ) = 0 → 2 = ( ⟨“ 2 2 ”⟩ ‘ ( 𝑥 − 1 ) ) )
23	18 22	syl	⊢ ( 𝑥 = 1 → 2 = ( ⟨“ 2 2 ”⟩ ‘ ( 𝑥 − 1 ) ) )
24		fveq2	⊢ ( 𝑥 = 1 → ( ⟨“ 2 2 ”⟩ ‘ 𝑥 ) = ( ⟨“ 2 2 ”⟩ ‘ 1 ) )
25		s2fv1	⊢ ( 2 ∈ V → ( ⟨“ 2 2 ”⟩ ‘ 1 ) = 2 )
26	12 25	ax-mp	⊢ ( ⟨“ 2 2 ”⟩ ‘ 1 ) = 2
27	24 26	eqtr2di	⊢ ( 𝑥 = 1 → 2 = ( ⟨“ 2 2 ”⟩ ‘ 𝑥 ) )
28	15 23 27	3brtr3d	⊢ ( 𝑥 = 1 → ( ⟨“ 2 2 ”⟩ ‘ ( 𝑥 − 1 ) ) I ( ⟨“ 2 2 ”⟩ ‘ 𝑥 ) )
29	7 10 28	3syl	⊢ ( 𝑥 ∈ ( dom ⟨“ 2 2 ”⟩ ∖ { 0 } ) → ( ⟨“ 2 2 ”⟩ ‘ ( 𝑥 − 1 ) ) I ( ⟨“ 2 2 ”⟩ ‘ 𝑥 ) )
30	29	rgen	⊢ ∀ 𝑥 ∈ ( dom ⟨“ 2 2 ”⟩ ∖ { 0 } ) ( ⟨“ 2 2 ”⟩ ‘ ( 𝑥 − 1 ) ) I ( ⟨“ 2 2 ”⟩ ‘ 𝑥 )
31		ischn	⊢ ( ⟨“ 2 2 ”⟩ ∈ ( I Chain ℤ ) ↔ ( ⟨“ 2 2 ”⟩ ∈ Word ℤ ∧ ∀ 𝑥 ∈ ( dom ⟨“ 2 2 ”⟩ ∖ { 0 } ) ( ⟨“ 2 2 ”⟩ ‘ ( 𝑥 − 1 ) ) I ( ⟨“ 2 2 ”⟩ ‘ 𝑥 ) ) )
32	3 30 31	mpbir2an	⊢ ⟨“ 2 2 ”⟩ ∈ ( I Chain ℤ )