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 eldifbd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ¬ 𝑥 ∈ { 0 } )
25 velsn ⊢ ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
26 24 25 sylnib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ¬ 𝑥 = 0 )
27 26 neqned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ≠ 0 )
28 elnnne0 ⊢ ( 𝑥 ∈ ℕ ↔ ( 𝑥 ∈ ℕ0 ∧ 𝑥 ≠ 0 ) )
29 22 27 28 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ℕ )
30 nnm1ge0 ⊢ ( 𝑥 ∈ ℕ → 0 ≤ ( 𝑥 − 1 ) )
31 29 30 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 0 ≤ ( 𝑥 − 1 ) )
32 22 nn0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ℝ )
33 peano2rem ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 − 1 ) ∈ ℝ )
34 32 33 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑥 − 1 ) ∈ ℝ )
35 lencl ⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
36 7 35 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
38 37 nn0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ♯ ‘ 𝐼 ) ∈ ℝ )
39 32 ltm1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑥 − 1 ) < 𝑥 )
40 11 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ dom ( 𝑊 ∘ 𝐼 ) )
41 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → dom ( 𝑊 ∘ 𝐼 ) = ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) )
42 40 41 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) )
43 elfzolt2 ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → 𝑥 < ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) )
44 42 43 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 < ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) )
45 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) )
46 44 45 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 < ( ♯ ‘ 𝐼 ) )
47 34 32 38 39 46 lttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑥 − 1 ) < ( ♯ ‘ 𝐼 ) )
48 elfzoelz ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) → 𝑥 ∈ ℤ )
49 19 48 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ℤ )
50 peano2zm ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 − 1 ) ∈ ℤ )
51 49 50 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑥 − 1 ) ∈ ℤ )
52 0zd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 0 ∈ ℤ )
53 36 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℤ )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ♯ ‘ 𝐼 ) ∈ ℤ )
55 elfzo ⊢ ( ( ( 𝑥 − 1 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ ( ♯ ‘ 𝐼 ) ∈ ℤ ) → ( ( 𝑥 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ( 0 ≤ ( 𝑥 − 1 ) ∧ ( 𝑥 − 1 ) < ( ♯ ‘ 𝐼 ) ) ) )
56 51 52 54 55 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ( 𝑥 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ( 0 ≤ ( 𝑥 − 1 ) ∧ ( 𝑥 − 1 ) < ( ♯ ‘ 𝐼 ) ) ) )
57 31 47 56 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑥 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
58 10 57 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
59 elfzonn0 ⊢ ( ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ℕ0 )
60 58 59 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ℕ0 )
61 elfzoelz ⊢ ( ( 𝐼 ‘ 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐼 ‘ 𝑥 ) ∈ ℤ )
62 20 61 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝐼 ‘ 𝑥 ) ∈ ℤ )
63 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
64 wrddm ⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → dom 𝐼 = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
65 7 64 syl ⊢ ( 𝜑 → dom 𝐼 = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
66 15 13 65 3eqtr4d ⊢ ( 𝜑 → dom ( 𝑊 ∘ 𝐼 ) = dom 𝐼 )
67 66 difeq1d ⊢ ( 𝜑 → ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) = ( dom 𝐼 ∖ { 0 } ) )
68 67 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ↔ 𝑥 ∈ ( dom 𝐼 ∖ { 0 } ) ) )
69 68 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → 𝑥 ∈ ( dom 𝐼 ∖ { 0 } ) )
70 63 69 chnltm1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝐼 ‘ ( 𝑥 − 1 ) ) < ( 𝐼 ‘ 𝑥 ) )
71 elfzo0z ⊢ ( ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ( 0 ..^ ( 𝐼 ‘ 𝑥 ) ) ↔ ( ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ℕ0 ∧ ( 𝐼 ‘ 𝑥 ) ∈ ℤ ∧ ( 𝐼 ‘ ( 𝑥 − 1 ) ) < ( 𝐼 ‘ 𝑥 ) ) )
72 60 62 70 71 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝐼 ‘ ( 𝑥 − 1 ) ) ∈ ( 0 ..^ ( 𝐼 ‘ 𝑥 ) ) )
73 5 6 20 72 chnlt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( 𝑊 ‘ ( 𝐼 ‘ ( 𝑥 − 1 ) ) ) < ( 𝑊 ‘ ( 𝐼 ‘ 𝑥 ) ) )
74 10 57 fvco3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ( 𝑊 ∘ 𝐼 ) ‘ ( 𝑥 − 1 ) ) = ( 𝑊 ‘ ( 𝐼 ‘ ( 𝑥 − 1 ) ) ) )
75 10 19 fvco3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ( 𝑊 ∘ 𝐼 ) ‘ 𝑥 ) = ( 𝑊 ‘ ( 𝐼 ‘ 𝑥 ) ) )
76 73 74 75 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ) → ( ( 𝑊 ∘ 𝐼 ) ‘ ( 𝑥 − 1 ) ) < ( ( 𝑊 ∘ 𝐼 ) ‘ 𝑥 ) )
77 76 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ( ( 𝑊 ∘ 𝐼 ) ‘ ( 𝑥 − 1 ) ) < ( ( 𝑊 ∘ 𝐼 ) ‘ 𝑥 ) )
78 ischn ⊢ ( ( 𝑊 ∘ 𝐼 ) ∈ ( < Chain 𝐴 ) ↔ ( ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 ∧ ∀ 𝑥 ∈ ( dom ( 𝑊 ∘ 𝐼 ) ∖ { 0 } ) ( ( 𝑊 ∘ 𝐼 ) ‘ ( 𝑥 − 1 ) ) < ( ( 𝑊 ∘ 𝐼 ) ‘ 𝑥 ) ) )
79 4 77 78 sylanbrc ⊢ ( 𝜑 → ( 𝑊 ∘ 𝐼 ) ∈ ( < Chain 𝐴 ) )