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 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
chnccats1.2 ⊢ ( 𝜑 → 𝑇 ∈ ( < Chain 𝐴 ) )
chnccats1.3 ⊢ ( 𝜑 → ( 𝑇 = ∅ ∨ ( lastS ‘ 𝑇 ) < 𝑋 ) )
Assertion chnccats1 ( 𝜑 → ( 𝑇 ++ ⟨“ 𝑋 ”⟩ ) ∈ ( < Chain 𝐴 ) )

Proof

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