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 ⊢ ( 𝜑 → 𝑊 ∈ ( < Chain 𝐴 ) )
chnsubseq.2 ⊢ ( 𝜑 → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
chnsubseq.3 ⊢ ( 𝜑 → < Po 𝐴 )
Assertion chnsubseq ( 𝜑 → ( 𝑊 ∘ 𝐼 ) ∈ ( < Chain 𝐴 ) )

Proof

Step Hyp Ref Expression
1 chnsubseq.1 ⊢ ( 𝜑 → 𝑊 ∈ ( < Chain 𝐴 ) )
2 chnsubseq.2 ⊢ ( 𝜑 → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
3 chnsubseq.3 ⊢ ( 𝜑 → < Po 𝐴 )
4 1 2 chnsubseqword ⊢ ( 𝜑 → ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 )
5 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → < Po 𝐴 )
6 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑊 ∈ ( < Chain 𝐴 ) )
7 2 chnwrd ⊢ ( 𝜑 → 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
9 wrdf ⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
10 8 9 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝐼 : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
11 eldifi ⊢ ( 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) → 𝑥 ∈ dom ( 𝑊 ∘ 𝐼 ) )
12 wrddm ⊢ ( ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 → dom ( 𝑊 ∘ 𝐼 ) = ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) )
13 4 12 syl ⊢ ( 𝜑 → dom ( 𝑊 ∘ 𝐼 ) = ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) )
14 1 2 chnsubseqwl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) )
15 14 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
16 13 15 eqtrd ⊢ ( 𝜑 → dom ( 𝑊 ∘ 𝐼 ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
17 16 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom ( 𝑊 ∘ 𝐼 ) ↔ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ) )
18 17 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝑊 ∘ 𝐼 ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
19 11 18 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
20 10 19 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝐼 ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
21 elfzonn0 ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) → 𝑥 ∈ ℕ0 )
22 19 21 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ℕ0 )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) )
24 23 eldifsnbd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ≠ 0 )
25 elnnne0 ⊢ ( 𝑥 ∈ ℕ ↔ ( 𝑥 ∈ ℕ0 ∧ 𝑥 ≠ 0 ) )
26 22 24 25 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ℕ )
27 nnm1ge0 ⊢ ( 𝑥 ∈ ℕ → 0 ≤ ( 𝑥 − 1 ) )
28 26 27 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 0 ≤ ( 𝑥 − 1 ) )
29 22 nn0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ℝ )
30 peano2rem ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 − 1 ) ∈ ℝ )
31 29 30 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑥 − 1 ) ∈ ℝ )
32 lencl ⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
33 7 32 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
35 34 nn0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ♯ ‘ 𝐼 ) ∈ ℝ )
36 29 ltm1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑥 − 1 ) < 𝑥 )
37 11 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ dom ( 𝑊 ∘ 𝐼 ) )
38 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → dom ( 𝑊 ∘ 𝐼 ) = ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) )
39 37 38 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) )
40 elfzolt2 ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → 𝑥 < ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) )
41 39 40 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 < ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) )
42 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) )
43 41 42 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 < ( ♯ ‘ 𝐼 ) )
44 31 29 35 36 43 lttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑥 − 1 ) < ( ♯ ‘ 𝐼 ) )
45 elfzoelz ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) → 𝑥 ∈ ℤ )
46 peano2zm ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 − 1 ) ∈ ℤ )
47 19 45 46 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑥 − 1 ) ∈ ℤ )
48 0zd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 0 ∈ ℤ )
49 33 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℤ )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ♯ ‘ 𝐼 ) ∈ ℤ )
51 elfzo ⊢ ( ( ( 𝑥 − 1 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ ( ♯ ‘ 𝐼 ) ∈ ℤ ) → ( ( 𝑥 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ( 0 ≤ ( 𝑥 − 1 ) ∧ ( 𝑥 − 1 ) < ( ♯ ‘ 𝐼 ) ) ) )
52 47 48 50 51 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ( 𝑥 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ( 0 ≤ ( 𝑥 − 1 ) ∧ ( 𝑥 − 1 ) < ( ♯ ‘ 𝐼 ) ) ) )
53 28 44 52 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑥 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
54 10 53 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
55 elfzonn0 ⊢ ( ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ℕ0 )
56 54 55 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ℕ0 )
57 elfzoelz ⊢ ( ( 𝐼 ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐼 ‘ 𝑥 ) ∈ ℤ )
58 20 57 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝐼 ‘ 𝑥 ) ∈ ℤ )
59 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
60 wrddm ⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → dom 𝐼 = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
61 7 60 syl ⊢ ( 𝜑 → dom 𝐼 = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
62 15 13 61 3eqtr4d ⊢ ( 𝜑 → dom ( 𝑊 ∘ 𝐼 ) = dom 𝐼 )
63 62 difeq1d ⊢ ( 𝜑 → ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) = ( dom 𝐼 ∖ { 0 } ) )
64 63 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ↔ 𝑥 ∈ ( dom 𝐼 ∖ { 0 } ) ) )
65 64 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ( dom 𝐼 ∖ { 0 } ) )
66 59 65 chnltm1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝐼 ‘ ( 𝑥 − 1 ) ) < ( 𝐼 ‘ 𝑥 ) )
67 elfzo0z ⊢ ( ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ( 0 ..^ ( 𝐼 ‘ 𝑥 ) ) ↔ ( ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ℕ0 ∧ ( 𝐼 ‘ 𝑥 ) ∈ ℤ ∧ ( 𝐼 ‘ ( 𝑥 − 1 ) ) < ( 𝐼 ‘ 𝑥 ) ) )
68 56 58 66 67 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ( 0 ..^ ( 𝐼 ‘ 𝑥 ) ) )
69 5 6 20 68 chnlt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑊 ‘ ( 𝐼 ‘ ( 𝑥 − 1 ) ) ) < ( 𝑊 ‘ ( 𝐼 ‘ 𝑥 ) ) )
70 10 53 fvco3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ( 𝑊 ∘ 𝐼 ) ‘ ( 𝑥 − 1 ) ) = ( 𝑊 ‘ ( 𝐼 ‘ ( 𝑥 − 1 ) ) ) )
71 10 19 fvco3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ( 𝑊 ∘ 𝐼 ) ‘ 𝑥 ) = ( 𝑊 ‘ ( 𝐼 ‘ 𝑥 ) ) )
72 69 70 71 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ( 𝑊 ∘ 𝐼 ) ‘ ( 𝑥 − 1 ) ) < ( ( 𝑊 ∘ 𝐼 ) ‘ 𝑥 ) )
73 72 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ( ( 𝑊 ∘ 𝐼 ) ‘ ( 𝑥 − 1 ) ) < ( ( 𝑊 ∘ 𝐼 ) ‘ 𝑥 ) )
74 ischn ⊢ ( ( 𝑊 ∘ 𝐼 ) ∈ ( < Chain 𝐴 ) ↔ ( ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 ∧ ∀ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ( ( 𝑊 ∘ 𝐼 ) ‘ ( 𝑥 − 1 ) ) < ( ( 𝑊 ∘ 𝐼 ) ‘ 𝑥 ) ) )
75 4 73 74 sylanbrc ⊢ ( 𝜑 → ( 𝑊 ∘ 𝐼 ) ∈ ( < Chain 𝐴 ) )