Metamath Proof Explorer

Theorem chnsubseq

Description: An order-preserving subsequence of an ordered chain is itself a chain. (Contributed by Ender Ting, 22-Jan-2026)

Ref Expression
Hypotheses chnsubseq.1 
|- ( ph -> W e. ( .< Chain A ) )
chnsubseq.2 
|- ( ph -> I e. ( < Chain ( 0 ..^ ( # ` W ) ) ) )
chnsubseq.3 
|- ( ph -> .< Po A )
Assertion chnsubseq 
|- ( ph -> ( W o. I ) e. ( .< Chain A ) )

Proof

Step Hyp Ref Expression
1 chnsubseq.1 
 |-  ( ph -> W e. ( .< Chain A ) )
2 chnsubseq.2 
 |-  ( ph -> I e. ( < Chain ( 0 ..^ ( # ` W ) ) ) )
3 chnsubseq.3 
 |-  ( ph -> .< Po A )
4 1 2 chnsubseqword 
 |-  ( ph -> ( W o. I ) e. Word A )
5 3 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> .< Po A )
6 1 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> W e. ( .< Chain A ) )
7 2 chnwrd 
 |-  ( ph -> I e. Word ( 0 ..^ ( # ` W ) ) )
8 7 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> I e. Word ( 0 ..^ ( # ` W ) ) )
9 wrdf 
 |-  ( I e. Word ( 0 ..^ ( # ` W ) ) -> I : ( 0 ..^ ( # ` I ) ) --> ( 0 ..^ ( # ` W ) ) )
10 8 9 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> I : ( 0 ..^ ( # ` I ) ) --> ( 0 ..^ ( # ` W ) ) )
11 eldifi 
 |-  ( x e. ( dom ( W o. I ) \ { 0 } ) -> x e. dom ( W o. I ) )
12 wrddm 
 |-  ( ( W o. I ) e. Word A -> dom ( W o. I ) = ( 0 ..^ ( # ` ( W o. I ) ) ) )
13 4 12 syl 
 |-  ( ph -> dom ( W o. I ) = ( 0 ..^ ( # ` ( W o. I ) ) ) )
14 1 2 chnsubseqwl 
 |-  ( ph -> ( # ` ( W o. I ) ) = ( # ` I ) )
15 14 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( W o. I ) ) ) = ( 0 ..^ ( # ` I ) ) )
16 13 15 eqtrd 
 |-  ( ph -> dom ( W o. I ) = ( 0 ..^ ( # ` I ) ) )
17 16 eleq2d 
 |-  ( ph -> ( x e. dom ( W o. I ) <-> x e. ( 0 ..^ ( # ` I ) ) ) )
18 17 biimpa 
 |-  ( ( ph /\ x e. dom ( W o. I ) ) -> x e. ( 0 ..^ ( # ` I ) ) )
19 11 18 sylan2 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. ( 0 ..^ ( # ` I ) ) )
20 10 19 ffvelcdmd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( I ` x ) e. ( 0 ..^ ( # ` W ) ) )
21 elfzonn0 
 |-  ( x e. ( 0 ..^ ( # ` I ) ) -> x e. NN0 )
22 19 21 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. NN0 )
23 simpr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. ( dom ( W o. I ) \ { 0 } ) )
24 23 eldifbd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> -. x e. { 0 } )
25 velsn 
 |-  ( x e. { 0 } <-> x = 0 )
26 24 25 sylnib 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> -. x = 0 )
27 26 neqned 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x =/= 0 )
28 elnnne0 
 |-  ( x e. NN <-> ( x e. NN0 /\ x =/= 0 ) )
29 22 27 28 sylanbrc 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. NN )
30 nnm1ge0 
 |-  ( x e. NN -> 0 <_ ( x - 1 ) )
31 29 30 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> 0 <_ ( x - 1 ) )
32 22 nn0red 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. RR )
33 peano2rem 
 |-  ( x e. RR -> ( x - 1 ) e. RR )
34 32 33 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( x - 1 ) e. RR )
35 lencl 
 |-  ( I e. Word ( 0 ..^ ( # ` W ) ) -> ( # ` I ) e. NN0 )
36 7 35 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
37 36 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( # ` I ) e. NN0 )
38 37 nn0red 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( # ` I ) e. RR )
39 32 ltm1d 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( x - 1 ) < x )
40 11 adantl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. dom ( W o. I ) )
41 13 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> dom ( W o. I ) = ( 0 ..^ ( # ` ( W o. I ) ) ) )
42 40 41 eleqtrd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. ( 0 ..^ ( # ` ( W o. I ) ) ) )
43 elfzolt2 
 |-  ( x e. ( 0 ..^ ( # ` ( W o. I ) ) ) -> x < ( # ` ( W o. I ) ) )
44 42 43 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x < ( # ` ( W o. I ) ) )
45 14 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( # ` ( W o. I ) ) = ( # ` I ) )
46 44 45 breqtrd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x < ( # ` I ) )
47 34 32 38 39 46 lttrd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( x - 1 ) < ( # ` I ) )
48 elfzoelz 
 |-  ( x e. ( 0 ..^ ( # ` I ) ) -> x e. ZZ )
49 19 48 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. ZZ )
50 peano2zm 
 |-  ( x e. ZZ -> ( x - 1 ) e. ZZ )
51 49 50 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( x - 1 ) e. ZZ )
52 0zd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> 0 e. ZZ )
53 36 nn0zd 
 |-  ( ph -> ( # ` I ) e. ZZ )
54 53 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( # ` I ) e. ZZ )
55 elfzo 
 |-  ( ( ( x - 1 ) e. ZZ /\ 0 e. ZZ /\ ( # ` I ) e. ZZ ) -> ( ( x - 1 ) e. ( 0 ..^ ( # ` I ) ) <-> ( 0 <_ ( x - 1 ) /\ ( x - 1 ) < ( # ` I ) ) ) )
56 51 52 54 55 syl3anc 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( ( x - 1 ) e. ( 0 ..^ ( # ` I ) ) <-> ( 0 <_ ( x - 1 ) /\ ( x - 1 ) < ( # ` I ) ) ) )
57 31 47 56 mpbir2and 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( x - 1 ) e. ( 0 ..^ ( # ` I ) ) )
58 10 57 ffvelcdmd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( I ` ( x - 1 ) ) e. ( 0 ..^ ( # ` W ) ) )
59 elfzonn0 
 |-  ( ( I ` ( x - 1 ) ) e. ( 0 ..^ ( # ` W ) ) -> ( I ` ( x - 1 ) ) e. NN0 )
60 58 59 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( I ` ( x - 1 ) ) e. NN0 )
61 elfzoelz 
 |-  ( ( I ` x ) e. ( 0 ..^ ( # ` W ) ) -> ( I ` x ) e. ZZ )
62 20 61 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( I ` x ) e. ZZ )
63 2 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> I e. ( < Chain ( 0 ..^ ( # ` W ) ) ) )
64 wrddm 
 |-  ( I e. Word ( 0 ..^ ( # ` W ) ) -> dom I = ( 0 ..^ ( # ` I ) ) )
65 7 64 syl 
 |-  ( ph -> dom I = ( 0 ..^ ( # ` I ) ) )
66 15 13 65 3eqtr4d 
 |-  ( ph -> dom ( W o. I ) = dom I )
67 66 difeq1d 
 |-  ( ph -> ( dom ( W o. I ) \ { 0 } ) = ( dom I \ { 0 } ) )
68 67 eleq2d 
 |-  ( ph -> ( x e. ( dom ( W o. I ) \ { 0 } ) <-> x e. ( dom I \ { 0 } ) ) )
69 68 biimpa 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. ( dom I \ { 0 } ) )
70 63 69 chnltm1 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( I ` ( x - 1 ) ) < ( I ` x ) )
71 elfzo0z 
 |-  ( ( I ` ( x - 1 ) ) e. ( 0 ..^ ( I ` x ) ) <-> ( ( I ` ( x - 1 ) ) e. NN0 /\ ( I ` x ) e. ZZ /\ ( I ` ( x - 1 ) ) < ( I ` x ) ) )
72 60 62 70 71 syl3anbrc 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( I ` ( x - 1 ) ) e. ( 0 ..^ ( I ` x ) ) )
73 5 6 20 72 chnlt 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( W ` ( I ` ( x - 1 ) ) ) .< ( W ` ( I ` x ) ) )
74 10 57 fvco3d 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( ( W o. I ) ` ( x - 1 ) ) = ( W ` ( I ` ( x - 1 ) ) ) )
75 10 19 fvco3d 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( ( W o. I ) ` x ) = ( W ` ( I ` x ) ) )
76 73 74 75 3brtr4d 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( ( W o. I ) ` ( x - 1 ) ) .< ( ( W o. I ) ` x ) )
77 76 ralrimiva 
 |-  ( ph -> A. x e. ( dom ( W o. I ) \ { 0 } ) ( ( W o. I ) ` ( x - 1 ) ) .< ( ( W o. I ) ` x ) )
78 ischn 
 |-  ( ( W o. I ) e. ( .< Chain A ) <-> ( ( W o. I ) e. Word A /\ A. x e. ( dom ( W o. I ) \ { 0 } ) ( ( W o. I ) ` ( x - 1 ) ) .< ( ( W o. I ) ` x ) ) )
79 4 77 78 sylanbrc 
 |-  ( ph -> ( W o. I ) e. ( .< Chain A ) )