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 ⊢ ( 𝜑 → 𝑊 ∈ ( < Chain 𝐴 ) )
chnsubseq.2 ⊢ ( 𝜑 → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
Assertion chnsubseqword ( 𝜑 → ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 )

Proof

Step Hyp Ref Expression
1 chnsubseq.1 ⊢ ( 𝜑 → 𝑊 ∈ ( < Chain 𝐴 ) )
2 chnsubseq.2 ⊢ ( 𝜑 → 𝐼 ∈ ( < Chain ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
3 2 chnwrd ⊢ ( 𝜑 → 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
4 lencl ⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
5 3 4 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
6 dfclel ⊢ ( ( ♯ ‘ 𝐼 ) ∈ ℕ0 ↔ ∃ 𝑥 ( 𝑥 = ( ♯ ‘ 𝐼 ) ∧ 𝑥 ∈ ℕ0 ) )
7 5 6 sylib ⊢ ( 𝜑 → ∃ 𝑥 ( 𝑥 = ( ♯ ‘ 𝐼 ) ∧ 𝑥 ∈ ℕ0 ) )
8 exancom ⊢ ( ∃ 𝑥 ( 𝑥 = ( ♯ ‘ 𝐼 ) ∧ 𝑥 ∈ ℕ0 ) ↔ ∃ 𝑥 ( 𝑥 ∈ ℕ0 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) )
9 7 8 sylib ⊢ ( 𝜑 → ∃ 𝑥 ( 𝑥 ∈ ℕ0 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) )
10 df-rex ⊢ ( ∃ 𝑥 ∈ ℕ0 𝑥 = ( ♯ ‘ 𝐼 ) ↔ ∃ 𝑥 ( 𝑥 ∈ ℕ0 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) )
11 9 10 sylibr ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℕ0 𝑥 = ( ♯ ‘ 𝐼 ) )
12 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝑊 ∈ ( < Chain 𝐴 ) )
13 12 chnwrd ⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝑊 ∈ Word 𝐴 )
14 wrdf ⊢ ( 𝑊 ∈ Word 𝐴 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
15 13 14 syl ⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
16 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
17 wrdf ⊢ ( 𝐼 ∈ Word ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝐼 : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
19 15 18 fcod ⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ 𝐴 )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → 𝑥 = ( ♯ ‘ 𝐼 ) )
21 20 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → ( 0 ..^ 𝑥 ) = ( 0 ..^ ( ♯ ‘ 𝐼 ) ) )
22 21 feq2d ⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → ( ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ 𝑥 ) ⟶ 𝐴 ↔ ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ ( ♯ ‘ 𝐼 ) ) ⟶ 𝐴 ) )
23 19 22 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 = ( ♯ ‘ 𝐼 ) ) → ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ 𝑥 ) ⟶ 𝐴 )
24 23 ex ⊢ ( 𝜑 → ( 𝑥 = ( ♯ ‘ 𝐼 ) → ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ 𝑥 ) ⟶ 𝐴 ) )
25 24 a1d ⊢ ( 𝜑 → ( 𝑥 ∈ ℕ0 → ( 𝑥 = ( ♯ ‘ 𝐼 ) → ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ 𝑥 ) ⟶ 𝐴 ) ) )
26 25 reximdvai ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℕ0 𝑥 = ( ♯ ‘ 𝐼 ) → ∃ 𝑥 ∈ ℕ0 ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ 𝑥 ) ⟶ 𝐴 ) )
27 11 26 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℕ0 ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ 𝑥 ) ⟶ 𝐴 )
28 iswrd ⊢ ( ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 ↔ ∃ 𝑥 ∈ ℕ0 ( 𝑊 ∘ 𝐼 ) : ( 0 ..^ 𝑥 ) ⟶ 𝐴 )
29 27 28 sylibr ⊢ ( 𝜑 → ( 𝑊 ∘ 𝐼 ) ∈ Word 𝐴 )