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 ⊢ φ → W ∈ Chain A < ˙
chnsubseq.2 ⊢ φ → I ∈ Chain 0 ..^ W <
Assertion chnsubseqwl ⊢ φ → W ∘ I = I

Proof

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