Metamath Proof Explorer

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 
|- <" ZZ NN QQ "> e. ( ~~ Chain _V )

Proof

Step Hyp Ref Expression
1 s3cli 
 |-  <" ZZ NN QQ "> e. Word _V
2 zex 
 |-  ZZ e. _V
3 nnex 
 |-  NN e. _V
4 qex 
 |-  QQ e. _V
5 s3fn 
 |-  ( ( ZZ e. _V /\ NN e. _V /\ QQ e. _V ) -> <" ZZ NN QQ "> Fn { 0 , 1 , 2 } )
6 2 3 4 5 mp3an 
 |-  <" ZZ NN QQ "> Fn { 0 , 1 , 2 }
7 6 fndmi 
 |-  dom <" ZZ NN QQ "> = { 0 , 1 , 2 }
8 7 difeq1i 
 |-  ( dom <" ZZ NN QQ "> \ { 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 <" ZZ NN QQ "> \ { 0 } ) = { 1 , 2 }
16 15 eleq2i 
 |-  ( x e. ( dom <" ZZ NN QQ "> \ { 0 } ) <-> x e. { 1 , 2 } )
17 16 biimpi 
 |-  ( x e. ( dom <" ZZ NN QQ "> \ { 0 } ) -> x e. { 1 , 2 } )
18 elpri 
 |-  ( x e. { 1 , 2 } -> ( x = 1 \/ x = 2 ) )
19 znnen 
 |-  ZZ ~~ NN
20 19 a1i 
 |-  ( x = 1 -> ZZ ~~ NN )
21 oveq1 
 |-  ( x = 1 -> ( x - 1 ) = ( 1 - 1 ) )
22 1m1e0 
 |-  ( 1 - 1 ) = 0
23 21 22 eqtrdi 
 |-  ( x = 1 -> ( x - 1 ) = 0 )
24 23 fveq2d 
 |-  ( x = 1 -> ( <" ZZ NN QQ "> ` ( x - 1 ) ) = ( <" ZZ NN QQ "> ` 0 ) )
25 s3fv0 
 |-  ( ZZ e. _V -> ( <" ZZ NN QQ "> ` 0 ) = ZZ )
26 2 25 ax-mp 
 |-  ( <" ZZ NN QQ "> ` 0 ) = ZZ
27 24 26 eqtrdi 
 |-  ( x = 1 -> ( <" ZZ NN QQ "> ` ( x - 1 ) ) = ZZ )
28 fveq2 
 |-  ( x = 1 -> ( <" ZZ NN QQ "> ` x ) = ( <" ZZ NN QQ "> ` 1 ) )
29 s3fv1 
 |-  ( NN e. _V -> ( <" ZZ NN QQ "> ` 1 ) = NN )
30 3 29 ax-mp 
 |-  ( <" ZZ NN QQ "> ` 1 ) = NN
31 28 30 eqtrdi 
 |-  ( x = 1 -> ( <" ZZ NN QQ "> ` x ) = NN )
32 20 27 31 3brtr4d 
 |-  ( x = 1 -> ( <" ZZ NN QQ "> ` ( x - 1 ) ) ~~ ( <" ZZ NN QQ "> ` x ) )
33 qnnen 
 |-  QQ ~~ NN
34 33 ensymi 
 |-  NN ~~ QQ
35 34 a1i 
 |-  ( x = 2 -> NN ~~ QQ )
36 oveq1 
 |-  ( x = 2 -> ( x - 1 ) = ( 2 - 1 ) )
37 2m1e1 
 |-  ( 2 - 1 ) = 1
38 36 37 eqtrdi 
 |-  ( x = 2 -> ( x - 1 ) = 1 )
39 38 fveq2d 
 |-  ( x = 2 -> ( <" ZZ NN QQ "> ` ( x - 1 ) ) = ( <" ZZ NN QQ "> ` 1 ) )
40 39 30 eqtrdi 
 |-  ( x = 2 -> ( <" ZZ NN QQ "> ` ( x - 1 ) ) = NN )
41 fveq2 
 |-  ( x = 2 -> ( <" ZZ NN QQ "> ` x ) = ( <" ZZ NN QQ "> ` 2 ) )
42 s3fv2 
 |-  ( QQ e. _V -> ( <" ZZ NN QQ "> ` 2 ) = QQ )
43 4 42 ax-mp 
 |-  ( <" ZZ NN QQ "> ` 2 ) = QQ
44 41 43 eqtrdi 
 |-  ( x = 2 -> ( <" ZZ NN QQ "> ` x ) = QQ )
45 35 40 44 3brtr4d 
 |-  ( x = 2 -> ( <" ZZ NN QQ "> ` ( x - 1 ) ) ~~ ( <" ZZ NN QQ "> ` x ) )
46 32 45 jaoi 
 |-  ( ( x = 1 \/ x = 2 ) -> ( <" ZZ NN QQ "> ` ( x - 1 ) ) ~~ ( <" ZZ NN QQ "> ` x ) )
47 17 18 46 3syl 
 |-  ( x e. ( dom <" ZZ NN QQ "> \ { 0 } ) -> ( <" ZZ NN QQ "> ` ( x - 1 ) ) ~~ ( <" ZZ NN QQ "> ` x ) )
48 47 rgen 
 |-  A. x e. ( dom <" ZZ NN QQ "> \ { 0 } ) ( <" ZZ NN QQ "> ` ( x - 1 ) ) ~~ ( <" ZZ NN QQ "> ` x )
49 ischn 
 |-  ( <" ZZ NN QQ "> e. ( ~~ Chain _V ) <-> ( <" ZZ NN QQ "> e. Word _V /\ A. x e. ( dom <" ZZ NN QQ "> \ { 0 } ) ( <" ZZ NN QQ "> ` ( x - 1 ) ) ~~ ( <" ZZ NN QQ "> ` x ) ) )
50 1 48 49 mpbir2an 
 |-  <" ZZ NN QQ "> e. ( ~~ Chain _V )