Metamath Proof Explorer

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 "> e. ( _I Chain ZZ )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 s2cl 
 |-  ( ( 2 e. ZZ /\ 2 e. ZZ ) -> <" 2 2 "> e. Word ZZ )
3 1 1 2 mp2an 
 |-  <" 2 2 "> e. Word ZZ
4 s2dm 
 |-  dom <" 2 2 "> = { 0 , 1 }
5 4 difeq1i 
 |-  ( dom <" 2 2 "> \ { 0 } ) = ( { 0 , 1 } \ { 0 } )
6 5 eleq2i 
 |-  ( x e. ( dom <" 2 2 "> \ { 0 } ) <-> x e. ( { 0 , 1 } \ { 0 } ) )
7 6 biimpi 
 |-  ( x e. ( dom <" 2 2 "> \ { 0 } ) -> x e. ( { 0 , 1 } \ { 0 } ) )
8 difprsnss 
 |-  ( { 0 , 1 } \ { 0 } ) C_ { 1 }
9 8 sseli 
 |-  ( x e. ( { 0 , 1 } \ { 0 } ) -> x e. { 1 } )
10 9 elsnd 
 |-  ( x e. ( { 0 , 1 } \ { 0 } ) -> x = 1 )
11 eqid 
 |-  2 = 2
12 2ex 
 |-  2 e. _V
13 12 ideq 
 |-  ( 2 _I 2 <-> 2 = 2 )
14 11 13 mpbir 
 |-  2 _I 2
15 14 a1i 
 |-  ( x = 1 -> 2 _I 2 )
16 oveq1 
 |-  ( x = 1 -> ( x - 1 ) = ( 1 - 1 ) )
17 1m1e0 
 |-  ( 1 - 1 ) = 0
18 16 17 eqtrdi 
 |-  ( x = 1 -> ( x - 1 ) = 0 )
19 fveq2 
 |-  ( ( x - 1 ) = 0 -> ( <" 2 2 "> ` ( x - 1 ) ) = ( <" 2 2 "> ` 0 ) )
20 s2fv0 
 |-  ( 2 e. _V -> ( <" 2 2 "> ` 0 ) = 2 )
21 12 20 ax-mp 
 |-  ( <" 2 2 "> ` 0 ) = 2
22 19 21 eqtr2di 
 |-  ( ( x - 1 ) = 0 -> 2 = ( <" 2 2 "> ` ( x - 1 ) ) )
23 18 22 syl 
 |-  ( x = 1 -> 2 = ( <" 2 2 "> ` ( x - 1 ) ) )
24 fveq2 
 |-  ( x = 1 -> ( <" 2 2 "> ` x ) = ( <" 2 2 "> ` 1 ) )
25 s2fv1 
 |-  ( 2 e. _V -> ( <" 2 2 "> ` 1 ) = 2 )
26 12 25 ax-mp 
 |-  ( <" 2 2 "> ` 1 ) = 2
27 24 26 eqtr2di 
 |-  ( x = 1 -> 2 = ( <" 2 2 "> ` x ) )
28 15 23 27 3brtr3d 
 |-  ( x = 1 -> ( <" 2 2 "> ` ( x - 1 ) ) _I ( <" 2 2 "> ` x ) )
29 7 10 28 3syl 
 |-  ( x e. ( dom <" 2 2 "> \ { 0 } ) -> ( <" 2 2 "> ` ( x - 1 ) ) _I ( <" 2 2 "> ` x ) )
30 29 rgen 
 |-  A. x e. ( dom <" 2 2 "> \ { 0 } ) ( <" 2 2 "> ` ( x - 1 ) ) _I ( <" 2 2 "> ` x )
31 ischn 
 |-  ( <" 2 2 "> e. ( _I Chain ZZ ) <-> ( <" 2 2 "> e. Word ZZ /\ A. x e. ( dom <" 2 2 "> \ { 0 } ) ( <" 2 2 "> ` ( x - 1 ) ) _I ( <" 2 2 "> ` x ) ) )
32 3 30 31 mpbir2an 
 |-  <" 2 2 "> e. ( _I Chain ZZ )