Metamath Proof Explorer

Theorem chnccat

Description: Concatenate two chains. (Contributed by Ender Ting, 20-Jan-2026)

Ref Expression
Hypotheses chnccat.1 ⊢ φ → T ∈ Chain A < ˙
chnccat.2 ⊢ φ → U ∈ Chain A < ˙
chnccat.3 ⊢ φ → T = ∅ ∨ U = ∅ ∨ lastS ⁡ T < ˙ U ⁡ 0
Assertion chnccat ⊢ φ → T ++ U ∈ Chain A < ˙

Proof

Step Hyp Ref Expression
1 chnccat.1 ⊢ φ → T ∈ Chain A < ˙
2 chnccat.2 ⊢ φ → U ∈ Chain A < ˙
3 chnccat.3 ⊢ φ → T = ∅ ∨ U = ∅ ∨ lastS ⁡ T < ˙ U ⁡ 0
4 1 chnwrd ⊢ φ → T ∈ Word A
5 2 chnwrd ⊢ φ → U ∈ Word A
6 ccatcl ⊢ T ∈ Word A ∧ U ∈ Word A → T ++ U ∈ Word A
7 4 5 6 syl2anc ⊢ φ → T ++ U ∈ 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 T + U = 0 ..^ T ∖ 0 T + U
12 11 eleq2d ⊢ φ → n ∈ dom ⁡ T ∖ 0 T + U ↔ n ∈ 0 ..^ T ∖ 0 T + U
13 12 biimpar ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → n ∈ dom ⁡ T ∖ 0 T + U
14 snsspr1 ⊢ 0 ⊆ 0 T + U
15 sscon ⊢ 0 ⊆ 0 T + U → dom ⁡ T ∖ 0 T + U ⊆ dom ⁡ T ∖ 0
16 14 15 ax-mp ⊢ dom ⁡ T ∖ 0 T + U ⊆ dom ⁡ T ∖ 0
17 16 sseli ⊢ n ∈ dom ⁡ T ∖ 0 T + U → n ∈ dom ⁡ T ∖ 0
18 ischn ⊢ T ∈ Chain A < ˙ ↔ T ∈ Word A ∧ ∀ n ∈ dom ⁡ T ∖ 0 T ⁡ n − 1 < ˙ T ⁡ n
19 1 18 sylib ⊢ φ → T ∈ Word A ∧ ∀ n ∈ dom ⁡ T ∖ 0 T ⁡ n − 1 < ˙ T ⁡ n
20 19 simprd ⊢ φ → ∀ n ∈ dom ⁡ T ∖ 0 T ⁡ n − 1 < ˙ T ⁡ n
21 20 r19.21bi ⊢ φ ∧ n ∈ dom ⁡ T ∖ 0 → T ⁡ n − 1 < ˙ T ⁡ n
22 17 21 sylan2 ⊢ φ ∧ n ∈ dom ⁡ T ∖ 0 T + U → T ⁡ n − 1 < ˙ T ⁡ n
23 13 22 syldan ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → T ⁡ n − 1 < ˙ T ⁡ n
24 4 adantr ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → T ∈ Word A
25 5 adantr ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → U ∈ Word A
26 sscon ⊢ 0 ⊆ 0 T + U → 0 ..^ T ∖ 0 T + U ⊆ 0 ..^ T ∖ 0
27 14 26 ax-mp ⊢ 0 ..^ T ∖ 0 T + U ⊆ 0 ..^ T ∖ 0
28 27 sseli ⊢ n ∈ 0 ..^ T ∖ 0 T + U → n ∈ 0 ..^ T ∖ 0
29 28 adantl ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → n ∈ 0 ..^ T ∖ 0
30 lencl ⊢ T ∈ Word A → T ∈ ℕ 0
31 4 30 syl ⊢ φ → T ∈ ℕ 0
32 31 adantr ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → T ∈ ℕ 0
33 29 32 elfzodif0 ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → n − 1 ∈ 0 ..^ T
34 ccatval1 ⊢ T ∈ Word A ∧ U ∈ Word A ∧ n − 1 ∈ 0 ..^ T → T ++ U ⁡ n − 1 = T ⁡ n − 1
35 24 25 33 34 syl3anc ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → T ++ U ⁡ n − 1 = T ⁡ n − 1
36 simpr ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → n ∈ 0 ..^ T ∖ 0 T + U
37 36 eldifad ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → n ∈ 0 ..^ T
38 ccatval1 ⊢ T ∈ Word A ∧ U ∈ Word A ∧ n ∈ 0 ..^ T → T ++ U ⁡ n = T ⁡ n
39 24 25 37 38 syl3anc ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → T ++ U ⁡ n = T ⁡ n
40 23 35 39 3brtr4d ⊢ φ ∧ n ∈ 0 ..^ T ∖ 0 T + U → T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
41 40 adantlr ⊢ φ ∧ n ∈ dom ⁡ T ++ U ∖ 0 ∧ n ∈ 0 ..^ T ∖ 0 T + U → T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
42 simpr ⊢ φ ∧ n ∈ T ∖ 0 T + U → n ∈ T ∖ 0 T + U
43 42 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ T = ∅ → n ∈ T ∖ 0 T + U
44 noel ⊢ ¬ n ∈ ∅
45 fveq2 ⊢ T = ∅ → T = ∅
46 hash0 ⊢ ∅ = 0
47 45 46 eqtrdi ⊢ T = ∅ → T = 0
48 47 adantl ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ T = ∅ → T = 0
49 48 sneqd ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ T = ∅ → T = 0
50 49 difeq1d ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ T = ∅ → T ∖ 0 T + U = 0 ∖ 0 T + U
51 difpr ⊢ 0 ∖ 0 T + U = 0 ∖ 0 ∖ T + U
52 difid ⊢ 0 ∖ 0 = ∅
53 52 difeq1i ⊢ 0 ∖ 0 ∖ T + U = ∅ ∖ T + U
54 0dif ⊢ ∅ ∖ T + U = ∅
55 51 53 54 3eqtri ⊢ 0 ∖ 0 T + U = ∅
56 50 55 eqtrdi ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ T = ∅ → T ∖ 0 T + U = ∅
57 56 eleq2d ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ T = ∅ → n ∈ T ∖ 0 T + U ↔ n ∈ ∅
58 44 57 mtbiri ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ T = ∅ → ¬ n ∈ T ∖ 0 T + U
59 43 58 pm2.21dd ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ T = ∅ → T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
60 eldifi ⊢ n ∈ T ∖ 0 T + U → n ∈ T
61 60 elsnd ⊢ n ∈ T ∖ 0 T + U → n = T
62 61 ad2antlr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → n = T
63 vex ⊢ n ∈ V
64 63 a1i ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → n ∈ V
65 eldifn ⊢ n ∈ T ∖ 0 T + U → ¬ n ∈ 0 T + U
66 65 ad2antlr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → ¬ n ∈ 0 T + U
67 fveq2 ⊢ U = ∅ → U = ∅
68 67 46 eqtrdi ⊢ U = ∅ → U = 0
69 68 adantl ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → U = 0
70 69 oveq2d ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → T + U = T + 0
71 nn0cn ⊢ T ∈ ℕ 0 → T ∈ ℂ
72 4 30 71 3syl ⊢ φ → T ∈ ℂ
73 72 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U → T ∈ ℂ
74 73 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → T ∈ ℂ
75 74 addridd ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → T + 0 = T
76 70 75 eqtrd ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → T + U = T
77 76 preq2d ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → 0 T + U = 0 T
78 66 77 neleqtrd ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → ¬ n ∈ 0 T
79 64 78 nelpr2 ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → n ≠ T
80 62 79 pm2.21ddne ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = ∅ → T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
81 simpr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → lastS ⁡ T < ˙ U ⁡ 0
82 4 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U → T ∈ Word A
83 82 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → T ∈ Word A
84 5 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U → U ∈ Word A
85 84 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → U ∈ Word A
86 42 eldifad ⊢ φ ∧ n ∈ T ∖ 0 T + U → n ∈ T
87 86 elsnd ⊢ φ ∧ n ∈ T ∖ 0 T + U → n = T
88 87 oveq1d ⊢ φ ∧ n ∈ T ∖ 0 T + U → n − 1 = T − 1
89 82 30 syl ⊢ φ ∧ n ∈ T ∖ 0 T + U → T ∈ ℕ 0
90 sscon ⊢ 0 ⊆ 0 T + U → T ∖ 0 T + U ⊆ T ∖ 0
91 14 90 ax-mp ⊢ T ∖ 0 T + U ⊆ T ∖ 0
92 91 sseli ⊢ n ∈ T ∖ 0 T + U → n ∈ T ∖ 0
93 61 92 eqeltrrd ⊢ n ∈ T ∖ 0 T + U → T ∈ T ∖ 0
94 93 eldifbd ⊢ n ∈ T ∖ 0 T + U → ¬ T ∈ 0
95 94 adantl ⊢ φ ∧ n ∈ T ∖ 0 T + U → ¬ T ∈ 0
96 89 95 eldifd ⊢ φ ∧ n ∈ T ∖ 0 T + U → T ∈ ℕ 0 ∖ 0
97 dfn2 ⊢ ℕ = ℕ 0 ∖ 0
98 96 97 eleqtrrdi ⊢ φ ∧ n ∈ T ∖ 0 T + U → T ∈ ℕ
99 fzo0end ⊢ T ∈ ℕ → T − 1 ∈ 0 ..^ T
100 98 99 syl ⊢ φ ∧ n ∈ T ∖ 0 T + U → T − 1 ∈ 0 ..^ T
101 88 100 eqeltrd ⊢ φ ∧ n ∈ T ∖ 0 T + U → n − 1 ∈ 0 ..^ T
102 101 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → n − 1 ∈ 0 ..^ T
103 83 85 102 34 syl3anc ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → T ++ U ⁡ n − 1 = T ⁡ n − 1
104 61 oveq1d ⊢ n ∈ T ∖ 0 T + U → n − 1 = T − 1
105 104 adantl ⊢ φ ∧ n ∈ T ∖ 0 T + U → n − 1 = T − 1
106 105 fveq2d ⊢ φ ∧ n ∈ T ∖ 0 T + U → T ⁡ n − 1 = T ⁡ T − 1
107 lsw ⊢ T ∈ Word A → lastS ⁡ T = T ⁡ T − 1
108 82 107 syl ⊢ φ ∧ n ∈ T ∖ 0 T + U → lastS ⁡ T = T ⁡ T − 1
109 106 108 eqtr4d ⊢ φ ∧ n ∈ T ∖ 0 T + U → T ⁡ n − 1 = lastS ⁡ T
110 109 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → T ⁡ n − 1 = lastS ⁡ T
111 103 110 eqtrd ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → T ++ U ⁡ n − 1 = lastS ⁡ T
112 87 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → n = T
113 112 fveq2d ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → T ++ U ⁡ n = T ++ U ⁡ T
114 lencl ⊢ U ∈ Word A → U ∈ ℕ 0
115 5 114 syl ⊢ φ → U ∈ ℕ 0
116 115 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U → U ∈ ℕ 0
117 82 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = 0 → T ∈ Word A
118 117 30 71 3syl ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = 0 → T ∈ ℂ
119 simpr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = 0 → U = 0
120 118 119 jca ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = 0 → T ∈ ℂ ∧ U = 0
121 prid2g ⊢ T ∈ ℂ → T ∈ 0 T
122 121 adantr ⊢ T ∈ ℂ ∧ U = 0 → T ∈ 0 T
123 simpr ⊢ T ∈ ℂ ∧ U = 0 → U = 0
124 123 oveq2d ⊢ T ∈ ℂ ∧ U = 0 → T + U = T + 0
125 addrid ⊢ T ∈ ℂ → T + 0 = T
126 125 adantr ⊢ T ∈ ℂ ∧ U = 0 → T + 0 = T
127 124 126 eqtrd ⊢ T ∈ ℂ ∧ U = 0 → T + U = T
128 127 preq2d ⊢ T ∈ ℂ ∧ U = 0 → 0 T + U = 0 T
129 122 128 eleqtrrd ⊢ T ∈ ℂ ∧ U = 0 → T ∈ 0 T + U
130 129 snssd ⊢ T ∈ ℂ ∧ U = 0 → T ⊆ 0 T + U
131 ssdif0 ⊢ T ⊆ 0 T + U ↔ T ∖ 0 T + U = ∅
132 130 131 sylib ⊢ T ∈ ℂ ∧ U = 0 → T ∖ 0 T + U = ∅
133 nel02 ⊢ T ∖ 0 T + U = ∅ → ¬ n ∈ T ∖ 0 T + U
134 120 132 133 3syl ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ U = 0 → ¬ n ∈ T ∖ 0 T + U
135 134 ex ⊢ φ ∧ n ∈ T ∖ 0 T + U → U = 0 → ¬ n ∈ T ∖ 0 T + U
136 42 135 mt2d ⊢ φ ∧ n ∈ T ∖ 0 T + U → ¬ U = 0
137 136 neqned ⊢ φ ∧ n ∈ T ∖ 0 T + U → U ≠ 0
138 elnnne0 ⊢ U ∈ ℕ ↔ U ∈ ℕ 0 ∧ U ≠ 0
139 116 137 138 sylanbrc ⊢ φ ∧ n ∈ T ∖ 0 T + U → U ∈ ℕ
140 139 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → U ∈ ℕ
141 lbfzo0 ⊢ 0 ∈ 0 ..^ U ↔ U ∈ ℕ
142 140 141 sylibr ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → 0 ∈ 0 ..^ U
143 addlid ⊢ T ∈ ℂ → 0 + T = T
144 143 eqcomd ⊢ T ∈ ℂ → T = 0 + T
145 144 fveq2d ⊢ T ∈ ℂ → T ++ U ⁡ T = T ++ U ⁡ 0 + T
146 30 71 145 3syl ⊢ T ∈ Word A → T ++ U ⁡ T = T ++ U ⁡ 0 + T
147 146 3ad2ant1 ⊢ T ∈ Word A ∧ U ∈ Word A ∧ 0 ∈ 0 ..^ U → T ++ U ⁡ T = T ++ U ⁡ 0 + T
148 ccatval3 ⊢ T ∈ Word A ∧ U ∈ Word A ∧ 0 ∈ 0 ..^ U → T ++ U ⁡ 0 + T = U ⁡ 0
149 147 148 eqtrd ⊢ T ∈ Word A ∧ U ∈ Word A ∧ 0 ∈ 0 ..^ U → T ++ U ⁡ T = U ⁡ 0
150 83 85 142 149 syl3anc ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → T ++ U ⁡ T = U ⁡ 0
151 113 150 eqtrd ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → T ++ U ⁡ n = U ⁡ 0
152 81 111 151 3brtr4d ⊢ φ ∧ n ∈ T ∖ 0 T + U ∧ lastS ⁡ T < ˙ U ⁡ 0 → T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
153 3 adantr ⊢ φ ∧ n ∈ T ∖ 0 T + U → T = ∅ ∨ U = ∅ ∨ lastS ⁡ T < ˙ U ⁡ 0
154 59 80 152 153 mpjao3dan ⊢ φ ∧ n ∈ T ∖ 0 T + U → T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
155 154 adantlr ⊢ φ ∧ n ∈ dom ⁡ T ++ U ∖ 0 ∧ n ∈ T ∖ 0 T + U → T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
156 simpr ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n ∈ T ..^ T + U ∖ T ∖ 0 T + U
157 eldifi ⊢ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n ∈ T ..^ T + U ∖ T
158 157 eldifad ⊢ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n ∈ T ..^ T + U
159 elfzoelz ⊢ n ∈ T ..^ T + U → n ∈ ℤ
160 158 159 syl ⊢ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n ∈ ℤ
161 zcn ⊢ n ∈ ℤ → n ∈ ℂ
162 156 160 161 3syl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n ∈ ℂ
163 1cnd ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → 1 ∈ ℂ
164 72 adantr ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → T ∈ ℂ
165 162 163 164 sub32d ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n - 1 - T = n - T - 1
166 165 fveq2d ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → U ⁡ n - 1 - T = U ⁡ n - T - 1
167 2 adantr ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → U ∈ Chain A < ˙
168 158 adantl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n ∈ T ..^ T + U
169 nn0z ⊢ U ∈ ℕ 0 → U ∈ ℤ
170 5 114 169 3syl ⊢ φ → U ∈ ℤ
171 170 adantr ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → U ∈ ℤ
172 fzosubel3 ⊢ n ∈ T ..^ T + U ∧ U ∈ ℤ → n − T ∈ 0 ..^ U
173 168 171 172 syl2anc ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n − T ∈ 0 ..^ U
174 simpl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → φ
175 156 eldifad ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n ∈ T ..^ T + U ∖ T
176 174 175 jca ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → φ ∧ n ∈ T ..^ T + U ∖ T
177 eldifi ⊢ n ∈ T ..^ T + U ∖ T → n ∈ T ..^ T + U
178 177 159 161 3syl ⊢ n ∈ T ..^ T + U ∖ T → n ∈ ℂ
179 178 adantl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n ∈ ℂ
180 72 adantr ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → T ∈ ℂ
181 eldifsni ⊢ n ∈ T ..^ T + U ∖ T → n ≠ T
182 181 adantl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n ≠ T
183 179 180 182 subne0d ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n − T ≠ 0
184 nelsn ⊢ n − T ≠ 0 → ¬ n − T ∈ 0
185 176 183 184 3syl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → ¬ n − T ∈ 0
186 173 185 eldifd ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n − T ∈ 0 ..^ U ∖ 0
187 eqidd ⊢ φ → U = U
188 187 5 wrdfd ⊢ φ → U : 0 ..^ U ⟶ A
189 188 fdmd ⊢ φ → dom ⁡ U = 0 ..^ U
190 189 difeq1d ⊢ φ → dom ⁡ U ∖ 0 = 0 ..^ U ∖ 0
191 190 eleq2d ⊢ φ → n − T ∈ dom ⁡ U ∖ 0 ↔ n − T ∈ 0 ..^ U ∖ 0
192 191 biimpar ⊢ φ ∧ n − T ∈ 0 ..^ U ∖ 0 → n − T ∈ dom ⁡ U ∖ 0
193 186 192 syldan ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n − T ∈ dom ⁡ U ∖ 0
194 167 193 chnltm1 ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → U ⁡ n - T - 1 < ˙ U ⁡ n − T
195 166 194 eqbrtrd ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → U ⁡ n - 1 - T < ˙ U ⁡ n − T
196 4 adantr ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → T ∈ Word A
197 5 adantr ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → U ∈ Word A
198 177 159 syl ⊢ n ∈ T ..^ T + U ∖ T → n ∈ ℤ
199 198 adantl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n ∈ ℤ
200 nn0z ⊢ T ∈ ℕ 0 → T ∈ ℤ
201 4 30 200 3syl ⊢ φ → T ∈ ℤ
202 201 adantr ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → T ∈ ℤ
203 199 202 jca ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n ∈ ℤ ∧ T ∈ ℤ
204 elfzole1 ⊢ n ∈ T ..^ T + U → T ≤ n
205 177 204 syl ⊢ n ∈ T ..^ T + U ∖ T → T ≤ n
206 205 adantl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → T ≤ n
207 eldifn ⊢ n ∈ T ..^ T + U ∖ T → ¬ n ∈ T
208 velsn ⊢ n ∈ T ↔ n = T
209 208 biimpri ⊢ n = T → n ∈ T
210 209 necon3bi ⊢ ¬ n ∈ T → n ≠ T
211 210 necomd ⊢ ¬ n ∈ T → T ≠ n
212 207 211 syl ⊢ n ∈ T ..^ T + U ∖ T → T ≠ n
213 212 adantl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → T ≠ n
214 simp1r ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T ∈ ℤ
215 214 zred ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T ∈ ℝ
216 simp1l ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → n ∈ ℤ
217 216 zred ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → n ∈ ℝ
218 simp2 ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T ≤ n
219 simp3 ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T ≠ n
220 219 necomd ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → n ≠ T
221 215 217 218 220 leneltd ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T < n
222 simp1 ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → n ∈ ℤ ∧ T ∈ ℤ
223 222 ancomd ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T ∈ ℤ ∧ n ∈ ℤ
224 zltp1le ⊢ T ∈ ℤ ∧ n ∈ ℤ → T < n ↔ T + 1 ≤ n
225 223 224 syl ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T < n ↔ T + 1 ≤ n
226 221 225 mpbid ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T + 1 ≤ n
227 peano2re ⊢ T ∈ ℝ → T + 1 ∈ ℝ
228 215 227 syl ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T + 1 ∈ ℝ
229 1red ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → 1 ∈ ℝ
230 228 217 229 lesub1d ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T + 1 ≤ n ↔ T + 1 - 1 ≤ n − 1
231 zcn ⊢ T ∈ ℤ → T ∈ ℂ
232 1cnd ⊢ T ∈ ℤ → 1 ∈ ℂ
233 231 232 pncand ⊢ T ∈ ℤ → T + 1 - 1 = T
234 233 adantl ⊢ n ∈ ℤ ∧ T ∈ ℤ → T + 1 - 1 = T
235 234 3ad2ant1 ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T + 1 - 1 = T
236 235 breq1d ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T + 1 - 1 ≤ n − 1 ↔ T ≤ n − 1
237 230 236 bitrd ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T + 1 ≤ n ↔ T ≤ n − 1
238 226 237 mpbid ⊢ n ∈ ℤ ∧ T ∈ ℤ ∧ T ≤ n ∧ T ≠ n → T ≤ n − 1
239 203 206 213 238 syl3anc ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → T ≤ n − 1
240 199 zred ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n ∈ ℝ
241 peano2rem ⊢ n ∈ ℝ → n − 1 ∈ ℝ
242 240 241 syl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n − 1 ∈ ℝ
243 201 170 zaddcld ⊢ φ → T + U ∈ ℤ
244 243 adantr ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → T + U ∈ ℤ
245 244 zred ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → T + U ∈ ℝ
246 240 ltm1d ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n − 1 < n
247 elfzolt2 ⊢ n ∈ T ..^ T + U → n < T + U
248 177 247 syl ⊢ n ∈ T ..^ T + U ∖ T → n < T + U
249 248 adantl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n < T + U
250 242 240 245 246 249 lttrd ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n − 1 < T + U
251 peano2zm ⊢ n ∈ ℤ → n − 1 ∈ ℤ
252 199 251 syl ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n − 1 ∈ ℤ
253 elfzo ⊢ n − 1 ∈ ℤ ∧ T ∈ ℤ ∧ T + U ∈ ℤ → n − 1 ∈ T ..^ T + U ↔ T ≤ n − 1 ∧ n − 1 < T + U
254 252 202 244 253 syl3anc ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n − 1 ∈ T ..^ T + U ↔ T ≤ n − 1 ∧ n − 1 < T + U
255 239 250 254 mpbir2and ⊢ φ ∧ n ∈ T ..^ T + U ∖ T → n − 1 ∈ T ..^ T + U
256 157 255 sylan2 ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → n − 1 ∈ T ..^ T + U
257 ccatval2 ⊢ T ∈ Word A ∧ U ∈ Word A ∧ n − 1 ∈ T ..^ T + U → T ++ U ⁡ n − 1 = U ⁡ n - 1 - T
258 196 197 256 257 syl3anc ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → T ++ U ⁡ n − 1 = U ⁡ n - 1 - T
259 ccatval2 ⊢ T ∈ Word A ∧ U ∈ Word A ∧ n ∈ T ..^ T + U → T ++ U ⁡ n = U ⁡ n − T
260 196 197 168 259 syl3anc ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → T ++ U ⁡ n = U ⁡ n − T
261 195 258 260 3brtr4d ⊢ φ ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
262 261 adantlr ⊢ φ ∧ n ∈ dom ⁡ T ++ U ∖ 0 ∧ n ∈ T ..^ T + U ∖ T ∖ 0 T + U → T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
263 ccatlen ⊢ T ∈ Word A ∧ U ∈ Word A → T ++ U = T + U
264 4 5 263 syl2anc ⊢ φ → T ++ U = T + U
265 264 eqcomd ⊢ φ → T + U = T ++ U
266 265 7 wrdfd ⊢ φ → T ++ U : 0 ..^ T + U ⟶ A
267 266 fdmd ⊢ φ → dom ⁡ T ++ U = 0 ..^ T + U
268 267 difeq1d ⊢ φ → dom ⁡ T ++ U ∖ 0 = 0 ..^ T + U ∖ 0
269 fzonel ⊢ ¬ T + U ∈ 0 ..^ T + U
270 simpr ⊢ φ ∧ T + U ∈ 0 ..^ T + U ∖ 0 → T + U ∈ 0 ..^ T + U ∖ 0
271 270 eldifad ⊢ φ ∧ T + U ∈ 0 ..^ T + U ∖ 0 → T + U ∈ 0 ..^ T + U
272 271 ex ⊢ φ → T + U ∈ 0 ..^ T + U ∖ 0 → T + U ∈ 0 ..^ T + U
273 269 272 mtoi ⊢ φ → ¬ T + U ∈ 0 ..^ T + U ∖ 0
274 difsn ⊢ ¬ T + U ∈ 0 ..^ T + U ∖ 0 → 0 ..^ T + U ∖ 0 ∖ T + U = 0 ..^ T + U ∖ 0
275 274 eqcomd ⊢ ¬ T + U ∈ 0 ..^ T + U ∖ 0 → 0 ..^ T + U ∖ 0 = 0 ..^ T + U ∖ 0 ∖ T + U
276 273 275 syl ⊢ φ → 0 ..^ T + U ∖ 0 = 0 ..^ T + U ∖ 0 ∖ T + U
277 difpr ⊢ 0 ..^ T + U ∖ 0 T + U = 0 ..^ T + U ∖ 0 ∖ T + U
278 276 277 eqtr4di ⊢ φ → 0 ..^ T + U ∖ 0 = 0 ..^ T + U ∖ 0 T + U
279 268 278 eqtrd ⊢ φ → dom ⁡ T ++ U ∖ 0 = 0 ..^ T + U ∖ 0 T + U
280 279 eleq2d ⊢ φ → n ∈ dom ⁡ T ++ U ∖ 0 ↔ n ∈ 0 ..^ T + U ∖ 0 T + U
281 eldif ⊢ n ∈ 0 ..^ T + U ∖ 0 T + U ↔ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U
282 280 281 bitrdi ⊢ φ → n ∈ dom ⁡ T ++ U ∖ 0 ↔ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U
283 simpr ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ 0 ..^ T → n ∈ 0 ..^ T
284 simplrr ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ 0 ..^ T → ¬ n ∈ 0 T + U
285 283 284 eldifd ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ 0 ..^ T → n ∈ 0 ..^ T ∖ 0 T + U
286 285 orcd ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ 0 ..^ T → n ∈ 0 ..^ T ∖ 0 T + U ∨ n ∈ T ∖ 0 T + U ∨ n ∈ T ..^ T + U ∖ T ∖ 0 T + U
287 exmidd ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → n ∈ T ∨ ¬ n ∈ T
288 idd ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → n ∈ T → n ∈ T
289 simplrr ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → ¬ n ∈ 0 T + U
290 288 289 jctird ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → n ∈ T → n ∈ T ∧ ¬ n ∈ 0 T + U
291 eldif ⊢ n ∈ T ∖ 0 T + U ↔ n ∈ T ∧ ¬ n ∈ 0 T + U
292 290 291 imbitrrdi ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → n ∈ T → n ∈ T ∖ 0 T + U
293 idd ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → ¬ n ∈ T → ¬ n ∈ T
294 simpr ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → n ∈ T ..^ T + U
295 293 294 jctild ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → ¬ n ∈ T → n ∈ T ..^ T + U ∧ ¬ n ∈ T
296 eldif ⊢ n ∈ T ..^ T + U ∖ T ↔ n ∈ T ..^ T + U ∧ ¬ n ∈ T
297 295 296 imbitrrdi ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → ¬ n ∈ T → n ∈ T ..^ T + U ∖ T
298 297 289 jctird ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → ¬ n ∈ T → n ∈ T ..^ T + U ∖ T ∧ ¬ n ∈ 0 T + U
299 eldif ⊢ n ∈ T ..^ T + U ∖ T ∖ 0 T + U ↔ n ∈ T ..^ T + U ∖ T ∧ ¬ n ∈ 0 T + U
300 298 299 imbitrrdi ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → ¬ n ∈ T → n ∈ T ..^ T + U ∖ T ∖ 0 T + U
301 292 300 orim12d ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → n ∈ T ∨ ¬ n ∈ T → n ∈ T ∖ 0 T + U ∨ n ∈ T ..^ T + U ∖ T ∖ 0 T + U
302 287 301 mpd ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → n ∈ T ∖ 0 T + U ∨ n ∈ T ..^ T + U ∖ T ∖ 0 T + U
303 302 olcd ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U ∧ n ∈ T ..^ T + U → n ∈ 0 ..^ T ∖ 0 T + U ∨ n ∈ T ∖ 0 T + U ∨ n ∈ T ..^ T + U ∖ T ∖ 0 T + U
304 201 anim1ci ⊢ φ ∧ n ∈ 0 ..^ T + U → n ∈ 0 ..^ T + U ∧ T ∈ ℤ
305 304 adantrr ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U → n ∈ 0 ..^ T + U ∧ T ∈ ℤ
306 fzospliti ⊢ n ∈ 0 ..^ T + U ∧ T ∈ ℤ → n ∈ 0 ..^ T ∨ n ∈ T ..^ T + U
307 305 306 syl ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U → n ∈ 0 ..^ T ∨ n ∈ T ..^ T + U
308 286 303 307 mpjaodan ⊢ φ ∧ n ∈ 0 ..^ T + U ∧ ¬ n ∈ 0 T + U → n ∈ 0 ..^ T ∖ 0 T + U ∨ n ∈ T ∖ 0 T + U ∨ n ∈ T ..^ T + U ∖ T ∖ 0 T + U
309 282 308 sylbida ⊢ φ ∧ n ∈ dom ⁡ T ++ U ∖ 0 → n ∈ 0 ..^ T ∖ 0 T + U ∨ n ∈ T ∖ 0 T + U ∨ n ∈ T ..^ T + U ∖ T ∖ 0 T + U
310 3orass ⊢ n ∈ 0 ..^ T ∖ 0 T + U ∨ n ∈ T ∖ 0 T + U ∨ n ∈ T ..^ T + U ∖ T ∖ 0 T + U ↔ n ∈ 0 ..^ T ∖ 0 T + U ∨ n ∈ T ∖ 0 T + U ∨ n ∈ T ..^ T + U ∖ T ∖ 0 T + U
311 309 310 sylibr ⊢ φ ∧ n ∈ dom ⁡ T ++ U ∖ 0 → n ∈ 0 ..^ T ∖ 0 T + U ∨ n ∈ T ∖ 0 T + U ∨ n ∈ T ..^ T + U ∖ T ∖ 0 T + U
312 41 155 262 311 mpjao3dan ⊢ φ ∧ n ∈ dom ⁡ T ++ U ∖ 0 → T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
313 312 ralrimiva ⊢ φ → ∀ n ∈ dom ⁡ T ++ U ∖ 0 T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
314 ischn ⊢ T ++ U ∈ Chain A < ˙ ↔ T ++ U ∈ Word A ∧ ∀ n ∈ dom ⁡ T ++ U ∖ 0 T ++ U ⁡ n − 1 < ˙ T ++ U ⁡ n
315 7 313 314 sylanbrc ⊢ φ → T ++ U ∈ Chain A < ˙