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 2 chnwrd ⊢ φ → I ∈ Word 0 ..^ W
4 lencl ⊢ I ∈ Word 0 ..^ W → I ∈ ℕ 0
5 3 4 syl ⊢ φ → I ∈ ℕ 0
6 dfclel ⊢ I ∈ ℕ 0 ↔ ∃ x x = I ∧ x ∈ ℕ 0
7 5 6 sylib ⊢ φ → ∃ x x = I ∧ x ∈ ℕ 0
8 exancom ⊢ ∃ x x = I ∧ x ∈ ℕ 0 ↔ ∃ x x ∈ ℕ 0 ∧ x = I
9 7 8 sylib ⊢ φ → ∃ x x ∈ ℕ 0 ∧ x = I
10 df-rex ⊢ ∃ x ∈ ℕ 0 x = I ↔ ∃ x x ∈ ℕ 0 ∧ x = I
11 9 10 sylibr ⊢ φ → ∃ x ∈ ℕ 0 x = I
12 1 adantr ⊢ φ ∧ x = I → W ∈ Chain A < ˙
13 12 chnwrd ⊢ φ ∧ x = I → W ∈ Word A
14 wrdf ⊢ W ∈ Word A → W : 0 ..^ W ⟶ A
15 13 14 syl ⊢ φ ∧ x = I → W : 0 ..^ W ⟶ A
16 3 adantr ⊢ φ ∧ x = I → I ∈ Word 0 ..^ W
17 wrdf ⊢ I ∈ Word 0 ..^ W → I : 0 ..^ I ⟶ 0 ..^ W
18 16 17 syl ⊢ φ ∧ x = I → I : 0 ..^ I ⟶ 0 ..^ W
19 15 18 fcod ⊢ φ ∧ x = I → W ∘ I : 0 ..^ I ⟶ A
20 simpr ⊢ φ ∧ x = I → x = I
21 20 oveq2d ⊢ φ ∧ x = I → 0 ..^ x = 0 ..^ I
22 21 feq2d ⊢ φ ∧ x = I → W ∘ I : 0 ..^ x ⟶ A ↔ W ∘ I : 0 ..^ I ⟶ A
23 19 22 mpbird ⊢ φ ∧ x = I → W ∘ I : 0 ..^ x ⟶ A
24 23 ex ⊢ φ → x = I → W ∘ I : 0 ..^ x ⟶ A
25 24 a1d ⊢ φ → x ∈ ℕ 0 → x = I → W ∘ I : 0 ..^ x ⟶ A
26 25 reximdvai ⊢ φ → ∃ x ∈ ℕ 0 x = I → ∃ x ∈ ℕ 0 W ∘ I : 0 ..^ x ⟶ A
27 11 26 mpd ⊢ φ → ∃ x ∈ ℕ 0 W ∘ I : 0 ..^ x ⟶ A
28 iswrd ⊢ W ∘ I ∈ Word A ↔ ∃ x ∈ ℕ 0 W ∘ I : 0 ..^ x ⟶ A
29 27 28 sylibr ⊢ φ → W ∘ I ∈ Word A