Metamath Proof Explorer

Theorem chnsubseqwl

Description: A subsequence of a chain has the same length as its indexing sequence. (Contributed by Ender Ting, 22-Jan-2026)

Ref Expression
Hypotheses chnsubseq.1 ⊢ ( 𝜑 → 𝑊 ∈ ( < Chain 𝐴 ) )
chnsubseq.2 ⊢ ( 𝜑 → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
Assertion chnsubseqwl ( 𝜑 → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 chnsubseq.1 ⊢ ( 𝜑 → 𝑊 ∈ ( < Chain 𝐴 ) )
2 chnsubseq.2 ⊢ ( 𝜑 → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
3 2 chnwrd ⊢ ( 𝜑 → 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
4 wrdf ⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
5 3 4 syl ⊢ ( 𝜑 → 𝐼 : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 5 frnd ⊢ ( 𝜑 → ran 𝐼 ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
7 1 chnwrd ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐴 )
8 wrddm ⊢ ( 𝑊 ∈ Word 𝐴 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
9 7 8 syl ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
10 6 9 sseqtrrd ⊢ ( 𝜑 → ran 𝐼 ⊆ dom 𝑊 )
11 dmcosseq ⊢ ( ran 𝐼 ⊆ dom 𝑊 → dom ( 𝑊 ∘ 𝐼 ) = dom 𝐼 )
12 10 11 syl ⊢ ( 𝜑 → dom ( 𝑊 ∘ 𝐼 ) = dom 𝐼 )
13 1 2 chnsubseqword ⊢ ( 𝜑 → ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 )
14 wrddm ⊢ ( ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 → dom ( 𝑊 ∘ 𝐼 ) = ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) )
15 13 14 syl ⊢ ( 𝜑 → dom ( 𝑊 ∘ 𝐼 ) = ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) )
16 wrddm ⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → dom 𝐼 = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
17 3 16 syl ⊢ ( 𝜑 → dom 𝐼 = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
18 12 15 17 3eqtr3d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
19 0z ⊢ 0 ∈ ℤ
20 lencl ⊢ ( ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ∈ ℕ0 )
21 13 20 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ∈ ℕ0 )
22 21 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ∈ ℤ )
23 simpr ⊢ ( ( 𝜑 ∧ 0 < ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → 0 < ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) )
24 fzoopth ⊢ ( ( 0 ∈ ℤ ∧ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ∈ ℤ ∧ 0 < ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ( 0 = 0 ∧ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) ) ) )
25 19 22 23 24 mp3an2ani ⊢ ( ( 𝜑 ∧ 0 < ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ( 0 = 0 ∧ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) ) ) )
26 eqid ⊢ 0 = 0
27 26 biantrur ⊢ ( ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) ↔ ( 0 = 0 ∧ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) ) )
28 25 27 bitr4di ⊢ ( ( 𝜑 ∧ 0 < ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) ) )
29 simpr ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) )
30 29 oveq2d ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( 0 ..^ 0 ) = ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) )
31 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
32 30 31 eqtr3di ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) = ∅ )
33 32 eqeq1d ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ∅ = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ) )
34 eqcom ⊢ ( ∅ = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) = ∅ )
35 33 34 bitrdi ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) = ∅ ) )
36 0zd ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → 0 ∈ ℤ )
37 lencl ⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
38 3 37 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
39 38 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℤ )
40 39 adantr ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( ♯ ‘ 𝐼 ) ∈ ℤ )
41 fzon ⊢ ( ( 0 ∈ ℤ ∧ ( ♯ ‘ 𝐼 ) ∈ ℤ ) → ( ( ♯ ‘ 𝐼 ) ≤ 0 ↔ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) = ∅ ) )
42 36 40 41 syl2anc ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( ( ♯ ‘ 𝐼 ) ≤ 0 ↔ ( 0 ..^ ( ♯ ‘ 𝐼 ) ) = ∅ ) )
43 nn0le0eq0 ⊢ ( ( ♯ ‘ 𝐼 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐼 ) ≤ 0 ↔ ( ♯ ‘ 𝐼 ) = 0 ) )
44 43 biimpa ⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐼 ) ≤ 0 ) → ( ♯ ‘ 𝐼 ) = 0 )
45 38 44 sylan ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐼 ) ≤ 0 ) → ( ♯ ‘ 𝐼 ) = 0 )
46 45 adantlr ⊢ ( ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) ∧ ( ♯ ‘ 𝐼 ) ≤ 0 ) → ( ♯ ‘ 𝐼 ) = 0 )
47 id ⊢ ( ( ♯ ‘ 𝐼 ) = 0 → ( ♯ ‘ 𝐼 ) = 0 )
48 0le0 ⊢ 0 ≤ 0
49 47 48 eqbrtrdi ⊢ ( ( ♯ ‘ 𝐼 ) = 0 → ( ♯ ‘ 𝐼 ) ≤ 0 )
50 49 adantl ⊢ ( ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) ∧ ( ♯ ‘ 𝐼 ) = 0 ) → ( ♯ ‘ 𝐼 ) ≤ 0 )
51 46 50 impbida ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( ( ♯ ‘ 𝐼 ) ≤ 0 ↔ ( ♯ ‘ 𝐼 ) = 0 ) )
52 eqcom ⊢ ( ( ♯ ‘ 𝐼 ) = 0 ↔ 0 = ( ♯ ‘ 𝐼 ) )
53 52 a1i ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( ( ♯ ‘ 𝐼 ) = 0 ↔ 0 = ( ♯ ‘ 𝐼 ) ) )
54 29 eqeq1d ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( 0 = ( ♯ ‘ 𝐼 ) ↔ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) ) )
55 51 53 54 3bitrd ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( ( ♯ ‘ 𝐼 ) ≤ 0 ↔ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) ) )
56 35 42 55 3bitr2d ⊢ ( ( 𝜑 ∧ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) → ( ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) ) )
57 21 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) )
58 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
59 21 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ∈ ℝ )
60 58 59 leloed ⊢ ( 𝜑 → ( 0 ≤ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ↔ ( 0 < ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ∨ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) ) )
61 57 60 mpbid ⊢ ( 𝜑 → ( 0 < ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ∨ 0 = ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) )
62 28 56 61 mpjaodan ⊢ ( 𝜑 → ( ( 0 ..^ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ↔ ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) ) )
63 18 62 mpbid ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∘ 𝐼 ) ) = ( ♯ ‘ 𝐼 ) )