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 eldifsnbd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x =/= 0 )
25 elnnne0 
 |-  ( x e. NN <-> ( x e. NN0 /\ x =/= 0 ) )
26 22 24 25 sylanbrc 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. NN )
27 nnm1ge0 
 |-  ( x e. NN -> 0 <_ ( x - 1 ) )
28 26 27 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> 0 <_ ( x - 1 ) )
29 22 nn0red 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. RR )
30 peano2rem 
 |-  ( x e. RR -> ( x - 1 ) e. RR )
31 29 30 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( x - 1 ) e. RR )
32 lencl 
 |-  ( I e. Word ( 0 ..^ ( # ` W ) ) -> ( # ` I ) e. NN0 )
33 7 32 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
34 33 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( # ` I ) e. NN0 )
35 34 nn0red 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( # ` I ) e. RR )
36 29 ltm1d 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( x - 1 ) < x )
37 11 adantl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. dom ( W o. I ) )
38 13 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> dom ( W o. I ) = ( 0 ..^ ( # ` ( W o. I ) ) ) )
39 37 38 eleqtrd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. ( 0 ..^ ( # ` ( W o. I ) ) ) )
40 elfzolt2 
 |-  ( x e. ( 0 ..^ ( # ` ( W o. I ) ) ) -> x < ( # ` ( W o. I ) ) )
41 39 40 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x < ( # ` ( W o. I ) ) )
42 14 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( # ` ( W o. I ) ) = ( # ` I ) )
43 41 42 breqtrd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x < ( # ` I ) )
44 31 29 35 36 43 lttrd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( x - 1 ) < ( # ` I ) )
45 elfzoelz 
 |-  ( x e. ( 0 ..^ ( # ` I ) ) -> x e. ZZ )
46 peano2zm 
 |-  ( x e. ZZ -> ( x - 1 ) e. ZZ )
47 19 45 46 3syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( x - 1 ) e. ZZ )
48 0zd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> 0 e. ZZ )
49 33 nn0zd 
 |-  ( ph -> ( # ` I ) e. ZZ )
50 49 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( # ` I ) e. ZZ )
51 elfzo 
 |-  ( ( ( x - 1 ) e. ZZ /\ 0 e. ZZ /\ ( # ` I ) e. ZZ ) -> ( ( x - 1 ) e. ( 0 ..^ ( # ` I ) ) <-> ( 0 <_ ( x - 1 ) /\ ( x - 1 ) < ( # ` I ) ) ) )
52 47 48 50 51 syl3anc 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( ( x - 1 ) e. ( 0 ..^ ( # ` I ) ) <-> ( 0 <_ ( x - 1 ) /\ ( x - 1 ) < ( # ` I ) ) ) )
53 28 44 52 mpbir2and 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( x - 1 ) e. ( 0 ..^ ( # ` I ) ) )
54 10 53 ffvelcdmd 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( I ` ( x - 1 ) ) e. ( 0 ..^ ( # ` W ) ) )
55 elfzonn0 
 |-  ( ( I ` ( x - 1 ) ) e. ( 0 ..^ ( # ` W ) ) -> ( I ` ( x - 1 ) ) e. NN0 )
56 54 55 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( I ` ( x - 1 ) ) e. NN0 )
57 elfzoelz 
 |-  ( ( I ` x ) e. ( 0 ..^ ( # ` W ) ) -> ( I ` x ) e. ZZ )
58 20 57 syl 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( I ` x ) e. ZZ )
59 2 adantr 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> I e. ( < Chain ( 0 ..^ ( # ` W ) ) ) )
60 wrddm 
 |-  ( I e. Word ( 0 ..^ ( # ` W ) ) -> dom I = ( 0 ..^ ( # ` I ) ) )
61 7 60 syl 
 |-  ( ph -> dom I = ( 0 ..^ ( # ` I ) ) )
62 15 13 61 3eqtr4d 
 |-  ( ph -> dom ( W o. I ) = dom I )
63 62 difeq1d 
 |-  ( ph -> ( dom ( W o. I ) \ { 0 } ) = ( dom I \ { 0 } ) )
64 63 eleq2d 
 |-  ( ph -> ( x e. ( dom ( W o. I ) \ { 0 } ) <-> x e. ( dom I \ { 0 } ) ) )
65 64 biimpa 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> x e. ( dom I \ { 0 } ) )
66 59 65 chnltm1 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( I ` ( x - 1 ) ) < ( I ` x ) )
67 elfzo0z 
 |-  ( ( I ` ( x - 1 ) ) e. ( 0 ..^ ( I ` x ) ) <-> ( ( I ` ( x - 1 ) ) e. NN0 /\ ( I ` x ) e. ZZ /\ ( I ` ( x - 1 ) ) < ( I ` x ) ) )
68 56 58 66 67 syl3anbrc 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( I ` ( x - 1 ) ) e. ( 0 ..^ ( I ` x ) ) )
69 5 6 20 68 chnlt 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( W ` ( I ` ( x - 1 ) ) ) .< ( W ` ( I ` x ) ) )
70 10 53 fvco3d 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( ( W o. I ) ` ( x - 1 ) ) = ( W ` ( I ` ( x - 1 ) ) ) )
71 10 19 fvco3d 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( ( W o. I ) ` x ) = ( W ` ( I ` x ) ) )
72 69 70 71 3brtr4d 
 |-  ( ( ph /\ x e. ( dom ( W o. I ) \ { 0 } ) ) -> ( ( W o. I ) ` ( x - 1 ) ) .< ( ( W o. I ) ` x ) )
73 72 ralrimiva 
 |-  ( ph -> A. x e. ( dom ( W o. I ) \ { 0 } ) ( ( W o. I ) ` ( x - 1 ) ) .< ( ( W o. I ) ` x ) )
74 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 ) ) )
75 4 73 74 sylanbrc 
 |-  ( ph -> ( W o. I ) e. ( .< Chain A ) )