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 
|- ( ph -> X e. A )
chnccats1.2 
|- ( ph -> T e. ( .< Chain A ) )
chnccats1.3 
|- ( ph -> ( T = (/) \/ ( lastS ` T ) .< X ) )
Assertion chnccats1 
|- ( ph -> ( T ++ <" X "> ) e. ( .< Chain A ) )

Proof

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