Metamath Proof Explorer

Theorem chnccats1

Description: Extend a chain with a single element. (Contributed by Thierry Arnoux, 19-Oct-2025)

Ref Expression
Hypotheses chnccats1.1 ⊢ φ → X ∈ A
chnccats1.2 ⊢ φ → T ∈ Chain A < ˙
chnccats1.3 ⊢ φ → T = ∅ ∨ lastS ⁡ T < ˙ X
Assertion chnccats1 ⊢ φ → T ++ ⟨“ X ”⟩ ∈ Chain A < ˙

Proof

Step Hyp Ref Expression
1 chnccats1.1 ⊢ φ → X ∈ A
2 chnccats1.2 ⊢ φ → T ∈ Chain A < ˙
3 chnccats1.3 ⊢ φ → T = ∅ ∨ lastS ⁡ T < ˙ X
4 2 chnwrd ⊢ φ → T ∈ Word A
5 1 s1cld ⊢ φ → ⟨“ X ”⟩ ∈ Word A
6 ccatcl ⊢ T ∈ Word A ∧ ⟨“ X ”⟩ ∈ Word A → T ++ ⟨“ X ”⟩ ∈ Word A
7 4 5 6 syl2anc ⊢ φ → T ++ ⟨“ X ”⟩ ∈ Word A
8 eqidd ⊢ φ → T = T
9 8 4 wrdfd ⊢ φ → T : 0 ..^ T ⟶ A
10 9 fdmd ⊢ φ → dom ⁡ T = 0 ..^ T
11 10 difeq1d ⊢ φ → dom ⁡ T ∖ 0 = 0 ..^ T ∖ 0
12 11 eleq2d ⊢ φ → n ∈ dom ⁡ T ∖ 0 ↔ n ∈ 0 ..^ T ∖ 0
13 12 biimpar ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 → n ∈ dom ⁡ T ∖ 0
14 ischn ⊢ T ∈ Chain A < ˙ ↔ T ∈ Word A ∧ ∀ n ∈ dom ⁡ T ∖ 0 T ⁡ n − 1 < ˙ T ⁡ n
15 2 14 sylib ⊢ φ → T ∈ Word A ∧ ∀ n ∈ dom ⁡ T ∖ 0 T ⁡ n − 1 < ˙ T ⁡ n
16 15 simprd ⊢ φ → ∀ n ∈ dom ⁡ T ∖ 0 T ⁡ n − 1 < ˙ T ⁡ n
17 16 r19.21bi ⊢ φ ∧ n ∈ dom ⁡ T ∖ 0 → T ⁡ n − 1 < ˙ T ⁡ n
18 13 17 syldan ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 → T ⁡ n − 1 < ˙ T ⁡ n
19 4 adantr ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 → T ∈ Word A
20 simpr ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 → n ∈ 0 ..^ T ∖ 0
21 lencl ⊢ T ∈ Word A → T ∈ ℕ 0
22 19 21 syl ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 → T ∈ ℕ 0
23 20 22 elfzodif0 ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 → n − 1 ∈ 0 ..^ T
24 ccats1val1 ⊢ T ∈ Word A ∧ n − 1 ∈ 0 ..^ T → T ++ ⟨“ X ”⟩ ⁡ n − 1 = T ⁡ n − 1
25 19 23 24 syl2anc ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 → T ++ ⟨“ X ”⟩ ⁡ n − 1 = T ⁡ n − 1
26 20 eldifad ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 → n ∈ 0 ..^ T
27 ccats1val1 ⊢ T ∈ Word A ∧ n ∈ 0 ..^ T → T ++ ⟨“ X ”⟩ ⁡ n = T ⁡ n
28 19 26 27 syl2anc ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 → T ++ ⟨“ X ”⟩ ⁡ n = T ⁡ n
29 18 25 28 3brtr4d ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 → T ++ ⟨“ X ”⟩ ⁡ n − 1 < ˙ T ++ ⟨“ X ”⟩ ⁡ n
30 29 adantlr ⊢ φ ∧ n ∈ dom ⁡ T ++ ⟨“ X ”⟩ ∖ 0 ∧ n ∈ 0 ..^ T ∖ 0 → T ++ ⟨“ X ”⟩ ⁡ n − 1 < ˙ T ++ ⟨“ X ”⟩ ⁡ n
31 simpr ⊢ φ ∧ n ∈ T ∖ 0 → n ∈ T ∖ 0
32 31 adantr ⊢ φ ∧ n ∈ T ∖ 0 ∧ T = ∅ → n ∈ T ∖ 0
33 noel ⊢ ¬ n ∈ ∅
34 fveq2 ⊢ T = ∅ → T = ∅
35 hash0 ⊢ ∅ = 0
36 34 35 eqtrdi ⊢ T = ∅ → T = 0
37 36 adantl ⊢ φ ∧ n ∈ T ∖ 0 ∧ T = ∅ → T = 0
38 37 sneqd ⊢ φ ∧ n ∈ T ∖ 0 ∧ T = ∅ → T = 0
39 38 difeq1d ⊢ φ ∧ n ∈ T ∖ 0 ∧ T = ∅ → T ∖ 0 = 0 ∖ 0
40 difid ⊢ 0 ∖ 0 = ∅
41 39 40 eqtrdi ⊢ φ ∧ n ∈ T ∖ 0 ∧ T = ∅ → T ∖ 0 = ∅
42 41 eleq2d ⊢ φ ∧ n ∈ T ∖ 0 ∧ T = ∅ → n ∈ T ∖ 0 ↔ n ∈ ∅
43 33 42 mtbiri ⊢ φ ∧ n ∈ T ∖ 0 ∧ T = ∅ → ¬ n ∈ T ∖ 0
44 32 43 pm2.21dd ⊢ φ ∧ n ∈ T ∖ 0 ∧ T = ∅ → T ++ ⟨“ X ”⟩ ⁡ n − 1 < ˙ T ++ ⟨“ X ”⟩ ⁡ n
45 simpr ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → lastS ⁡ T < ˙ X
46 31 eldifad ⊢ φ ∧ n ∈ T ∖ 0 → n ∈ T
47 46 elsnd ⊢ φ ∧ n ∈ T ∖ 0 → n = T
48 47 oveq1d ⊢ φ ∧ n ∈ T ∖ 0 → n − 1 = T − 1
49 48 adantr ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → n − 1 = T − 1
50 49 fveq2d ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → T ⁡ n − 1 = T ⁡ T − 1
51 4 ad2antrr ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → T ∈ Word A
52 4 adantr ⊢ φ ∧ n ∈ T ∖ 0 → T ∈ Word A
53 52 21 syl ⊢ φ ∧ n ∈ T ∖ 0 → T ∈ ℕ 0
54 47 31 eqeltrrd ⊢ φ ∧ n ∈ T ∖ 0 → T ∈ T ∖ 0
55 54 eldifbd ⊢ φ ∧ n ∈ T ∖ 0 → ¬ T ∈ 0
56 53 55 eldifd ⊢ φ ∧ n ∈ T ∖ 0 → T ∈ ℕ 0 ∖ 0
57 dfn2 ⊢ ℕ = ℕ 0 ∖ 0
58 56 57 eleqtrrdi ⊢ φ ∧ n ∈ T ∖ 0 → T ∈ ℕ
59 fzo0end ⊢ T ∈ ℕ → T − 1 ∈ 0 ..^ T
60 58 59 syl ⊢ φ ∧ n ∈ T ∖ 0 → T − 1 ∈ 0 ..^ T
61 48 60 eqeltrd ⊢ φ ∧ n ∈ T ∖ 0 → n − 1 ∈ 0 ..^ T
62 61 adantr ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → n − 1 ∈ 0 ..^ T
63 51 62 24 syl2anc ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → T ++ ⟨“ X ”⟩ ⁡ n − 1 = T ⁡ n − 1
64 lsw ⊢ T ∈ Word A → lastS ⁡ T = T ⁡ T − 1
65 51 64 syl ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → lastS ⁡ T = T ⁡ T − 1
66 50 63 65 3eqtr4d ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → T ++ ⟨“ X ”⟩ ⁡ n − 1 = lastS ⁡ T
67 47 adantr ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → n = T
68 67 fveq2d ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → T ++ ⟨“ X ”⟩ ⁡ n = T ++ ⟨“ X ”⟩ ⁡ T
69 1 ad2antrr ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → X ∈ A
70 eqidd ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → T = T
71 ccats1val2 ⊢ T ∈ Word A ∧ X ∈ A ∧ T = T → T ++ ⟨“ X ”⟩ ⁡ T = X
72 51 69 70 71 syl3anc ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → T ++ ⟨“ X ”⟩ ⁡ T = X
73 68 72 eqtrd ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → T ++ ⟨“ X ”⟩ ⁡ n = X
74 45 66 73 3brtr4d ⊢ φ ∧ n ∈ T ∖ 0 ∧ lastS ⁡ T < ˙ X → T ++ ⟨“ X ”⟩ ⁡ n − 1 < ˙ T ++ ⟨“ X ”⟩ ⁡ n
75 3 adantr ⊢ φ ∧ n ∈ T ∖ 0 → T = ∅ ∨ lastS ⁡ T < ˙ X
76 44 74 75 mpjaodan ⊢ φ ∧ n ∈ T ∖ 0 → T ++ ⟨“ X ”⟩ ⁡ n − 1 < ˙ T ++ ⟨“ X ”⟩ ⁡ n
77 76 adantlr ⊢ φ ∧ n ∈ dom ⁡ T ++ ⟨“ X ”⟩ ∖ 0 ∧ n ∈ T ∖ 0 → T ++ ⟨“ X ”⟩ ⁡ n − 1 < ˙ T ++ ⟨“ X ”⟩ ⁡ n
78 ccatws1len ⊢ T ∈ Word A → T ++ ⟨“ X ”⟩ = T + 1
79 4 78 syl ⊢ φ → T ++ ⟨“ X ”⟩ = T + 1
80 79 eqcomd ⊢ φ → T + 1 = T ++ ⟨“ X ”⟩
81 80 7 wrdfd ⊢ φ → T ++ ⟨“ X ”⟩ : 0 ..^ T + 1 ⟶ A
82 81 fdmd ⊢ φ → dom ⁡ T ++ ⟨“ X ”⟩ = 0 ..^ T + 1
83 4 21 syl ⊢ φ → T ∈ ℕ 0
84 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
85 83 84 eleqtrdi ⊢ φ → T ∈ ℤ ≥ 0
86 fzosplitsn ⊢ T ∈ ℤ ≥ 0 → 0 ..^ T + 1 = 0 ..^ T ∪ T
87 85 86 syl ⊢ φ → 0 ..^ T + 1 = 0 ..^ T ∪ T
88 82 87 eqtrd ⊢ φ → dom ⁡ T ++ ⟨“ X ”⟩ = 0 ..^ T ∪ T
89 88 difeq1d ⊢ φ → dom ⁡ T ++ ⟨“ X ”⟩ ∖ 0 = 0 ..^ T ∪ T ∖ 0
90 difundir ⊢ 0 ..^ T ∪ T ∖ 0 = 0 ..^ T ∖ 0 ∪ T ∖ 0
91 89 90 eqtrdi ⊢ φ → dom ⁡ T ++ ⟨“ X ”⟩ ∖ 0 = 0 ..^ T ∖ 0 ∪ T ∖ 0
92 91 eleq2d ⊢ φ → n ∈ dom ⁡ T ++ ⟨“ X ”⟩ ∖ 0 ↔ n ∈ 0 ..^ T ∖ 0 ∪ T ∖ 0
93 92 biimpa ⊢ φ ∧ n ∈ dom ⁡ T ++ ⟨“ X ”⟩ ∖ 0 → n ∈ 0 ..^ T ∖ 0 ∪ T ∖ 0
94 elun ⊢ n ∈ 0 ..^ T ∖ 0 ∪ T ∖ 0 ↔ n ∈ 0 ..^ T ∖ 0 ∨ n ∈ T ∖ 0
95 93 94 sylib ⊢ φ ∧ n ∈ dom ⁡ T ++ ⟨“ X ”⟩ ∖ 0 → n ∈ 0 ..^ T ∖ 0 ∨ n ∈ T ∖ 0
96 30 77 95 mpjaodan ⊢ φ ∧ n ∈ dom ⁡ T ++ ⟨“ X ”⟩ ∖ 0 → T ++ ⟨“ X ”⟩ ⁡ n − 1 < ˙ T ++ ⟨“ X ”⟩ ⁡ n
97 96 ralrimiva ⊢ φ → ∀ n ∈ dom ⁡ T ++ ⟨“ X ”⟩ ∖ 0 T ++ ⟨“ X ”⟩ ⁡ n − 1 < ˙ T ++ ⟨“ X ”⟩ ⁡ n
98 ischn ⊢ T ++ ⟨“ X ”⟩ ∈ Chain A < ˙ ↔ T ++ ⟨“ X ”⟩ ∈ Word A ∧ ∀ n ∈ dom ⁡ T ++ ⟨“ X ”⟩ ∖ 0 T ++ ⟨“ X ”⟩ ⁡ n − 1 < ˙ T ++ ⟨“ X ”⟩ ⁡ n
99 7 97 98 sylanbrc ⊢ φ → T ++ ⟨“ X ”⟩ ∈ Chain A < ˙