Metamath Proof Explorer

Theorem pfxchn

Description: A prefix of a chain is still a chain. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses chnwrd.1 ⊢ φ → C ∈ Chain A < ˙
pfxchn.2 ⊢ φ → L ∈ 0 … C
Assertion pfxchn ⊢ φ → C prefix L ∈ Chain A < ˙

Proof

Step Hyp Ref Expression
1 chnwrd.1 ⊢ φ → C ∈ Chain A < ˙
2 pfxchn.2 ⊢ φ → L ∈ 0 … C
3 1 chnwrd ⊢ φ → C ∈ Word A
4 pfxcl ⊢ C ∈ Word A → C prefix L ∈ Word A
5 3 4 syl ⊢ φ → C prefix L ∈ Word A
6 1 adantr ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → C ∈ Chain A < ˙
7 2 adantr ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → L ∈ 0 … C
8 elfzuz3 ⊢ L ∈ 0 … C → C ∈ ℤ ≥ L
9 fzoss2 ⊢ C ∈ ℤ ≥ L → 0 ..^ L ⊆ 0 ..^ C
10 7 8 9 3syl ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → 0 ..^ L ⊆ 0 ..^ C
11 simpr ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → n ∈ dom ⁡ C prefix L ∖ 0
12 11 eldifad ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → n ∈ dom ⁡ C prefix L
13 3 adantr ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → C ∈ Word A
14 pfxlen ⊢ C ∈ Word A ∧ L ∈ 0 … C → C prefix L = L
15 13 7 14 syl2anc ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → C prefix L = L
16 15 eqcomd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → L = C prefix L
17 5 adantr ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → C prefix L ∈ Word A
18 16 17 wrdfd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → C prefix L : 0 ..^ L ⟶ A
19 18 fdmd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → dom ⁡ C prefix L = 0 ..^ L
20 12 19 eleqtrd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → n ∈ 0 ..^ L
21 10 20 sseldd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → n ∈ 0 ..^ C
22 eqidd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → C = C
23 22 13 wrdfd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → C : 0 ..^ C ⟶ A
24 23 fdmd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → dom ⁡ C = 0 ..^ C
25 21 24 eleqtrrd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → n ∈ dom ⁡ C
26 eldifsni ⊢ n ∈ dom ⁡ C prefix L ∖ 0 → n ≠ 0
27 11 26 syl ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → n ≠ 0
28 25 27 eldifsnd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → n ∈ dom ⁡ C ∖ 0
29 6 28 chnltm1 ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → C ⁡ n − 1 < ˙ C ⁡ n
30 7 elfzelzd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → L ∈ ℤ
31 fzossrbm1 ⊢ L ∈ ℤ → 0 ..^ L − 1 ⊆ 0 ..^ L
32 30 31 syl ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → 0 ..^ L − 1 ⊆ 0 ..^ L
33 fzom1ne1 ⊢ n ∈ 0 ..^ L ∧ n ≠ 0 → n − 1 ∈ 0 ..^ L − 1
34 20 27 33 syl2anc ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → n − 1 ∈ 0 ..^ L − 1
35 32 34 sseldd ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → n − 1 ∈ 0 ..^ L
36 pfxfv ⊢ C ∈ Word A ∧ L ∈ 0 … C ∧ n − 1 ∈ 0 ..^ L → C prefix L ⁡ n − 1 = C ⁡ n − 1
37 13 7 35 36 syl3anc ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → C prefix L ⁡ n − 1 = C ⁡ n − 1
38 pfxfv ⊢ C ∈ Word A ∧ L ∈ 0 … C ∧ n ∈ 0 ..^ L → C prefix L ⁡ n = C ⁡ n
39 13 7 20 38 syl3anc ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → C prefix L ⁡ n = C ⁡ n
40 29 37 39 3brtr4d ⊢ φ ∧ n ∈ dom ⁡ C prefix L ∖ 0 → C prefix L ⁡ n − 1 < ˙ C prefix L ⁡ n
41 40 ralrimiva ⊢ φ → ∀ n ∈ dom ⁡ C prefix L ∖ 0 C prefix L ⁡ n − 1 < ˙ C prefix L ⁡ n
42 ischn ⊢ C prefix L ∈ Chain A < ˙ ↔ C prefix L ∈ Word A ∧ ∀ n ∈ dom ⁡ C prefix L ∖ 0 C prefix L ⁡ n − 1 < ˙ C prefix L ⁡ n
43 5 41 42 sylanbrc ⊢ φ → C prefix L ∈ Chain A < ˙