Metamath Proof Explorer

Theorem chnsubseqword

Description: A subsequence of a chain is a word. (Contributed by Ender Ting, 22-Jan-2026)

Ref Expression
Hypotheses chnsubseq.1 ⊢ φ → W ∈ Chain A < ˙
chnsubseq.2 ⊢ φ → I ∈ Chain 0 ..^ W <
Assertion chnsubseqword ⊢ φ → W ∘ I ∈ Word A

Proof

Step Hyp Ref Expression
1 chnsubseq.1 ⊢ φ → W ∈ Chain A < ˙
2 chnsubseq.2 ⊢ φ → I ∈ Chain 0 ..^ W <
3 1 adantr ⊢ φ ∧ x = I → W ∈ Chain A < ˙
4 3 chnwrd ⊢ φ ∧ x = I → W ∈ Word A
5 wrdf ⊢ W ∈ Word A → W : 0 ..^ W ⟶ A
6 4 5 syl ⊢ φ ∧ x = I → W : 0 ..^ W ⟶ A
7 2 chnwrd ⊢ φ → I ∈ Word 0 ..^ W
8 7 adantr ⊢ φ ∧ x = I → I ∈ Word 0 ..^ W
9 wrdf ⊢ I ∈ Word 0 ..^ W → I : 0 ..^ I ⟶ 0 ..^ W
10 8 9 syl ⊢ φ ∧ x = I → I : 0 ..^ I ⟶ 0 ..^ W
11 6 10 fcod ⊢ φ ∧ x = I → W ∘ I : 0 ..^ I ⟶ A
12 simpr ⊢ φ ∧ x = I → x = I
13 12 oveq2d ⊢ φ ∧ x = I → 0 ..^ x = 0 ..^ I
14 13 feq2d ⊢ φ ∧ x = I → W ∘ I : 0 ..^ x ⟶ A ↔ W ∘ I : 0 ..^ I ⟶ A
15 11 14 mpbird ⊢ φ ∧ x = I → W ∘ I : 0 ..^ x ⟶ A
16 lencl ⊢ I ∈ Word 0 ..^ W → I ∈ ℕ 0
17 7 16 syl ⊢ φ → I ∈ ℕ 0
18 15 17 rspcime ⊢ φ → ∃ x ∈ ℕ 0 W ∘ I : 0 ..^ x ⟶ A
19 iswrd ⊢ W ∘ I ∈ Word A ↔ ∃ x ∈ ℕ 0 W ∘ I : 0 ..^ x ⟶ A
20 18 19 sylibr ⊢ φ → W ∘ I ∈ Word A