swrdccat - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > swrdccat		Unicode version

Theorem swrdccat 11226

Description: The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018.)

**Hypothesis**
Ref	Expression
swrdccatin2.l	♯

**Assertion**
Ref	Expression
swrdccat	Word $/\$ Word $/\$ ♯ ++ substr substr ++ substr

**Proof of Theorem swrdccat**
Step	Hyp	Ref	Expression
1		swrdccatin2.l	. . . . 5 ♯
2	1	pfxccat3 11225	. . . 4 Word $/\$ Word $/\$ ♯ ++ substr substr substr substr ++ prefix
3	2	imp 124	. . 3 Word $/\$ Word $/\$ $/\$ ♯ ++ substr substr substr substr ++ prefix
4		lencl 11035	. . . . . 6 Word ♯
5	4	adantr 276	. . . . 5 Word $/\$ Word ♯
6	1	eqcomi 2211	. . . . . . 7 ♯
7	6	eleq1i 2273	. . . . . 6 ♯
8		elfz2nn0 10269	. . . . . . . . 9 $/\$ $/\$
9		iftrue 3584	. . . . . . . . . . . . . . . . . 18
10	9	adantl 277	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
11	10	opeq2d 3840	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
12	11	oveq2d 5983	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
13		0z 9418	. . . . . . . . . . . . . . . . 17
14		simprll 537	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
15	14	adantr 276	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
16	15	nn0zd 9528	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
17		simplrr 536	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
18	17	nn0zd 9528	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
19	16, 18	zsubcld 9535	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
20		zdcle 9484	. . . . . . . . . . . . . . . . 17 $/\$ DECID
21	13, 19, 20	sylancr 414	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ DECID
22		exmiddc 838	. . . . . . . . . . . . . . . . 17 DECID $\/$
23		iftrue 3584	. . . . . . . . . . . . . . . . . . . . . . 23
24	23	opeq1d 3839	. . . . . . . . . . . . . . . . . . . . . 22
25	24	oveq2d 5983	. . . . . . . . . . . . . . . . . . . . 21 substr substr
26	25	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
27		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word Word
28		nn0z 9427	. . . . . . . . . . . . . . . . . . . . . . . . 25
29		nn0z 9427	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
30	29	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
31		zsubcl 9448	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
32	30, 31	sylan 283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
33		nn0z 9427	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
34	33	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35		zsubcl 9448	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
36	34, 35	sylan 283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
37	32, 36	jca 306	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
38	28, 37	sylan2 286	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
39	27, 38	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
40		3anass 985	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ $/\$ Word $/\$ $/\$
41	39, 40	sylibr 134	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
42	41	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
43		nn0re 9339	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
44		nn0re 9339	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
45	43, 44	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
46		nn0re 9339	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47		subge0 8583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
48	47	adantlr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
49		simplr 528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
50		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
51		simpll 527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
52		letr 8190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
53	49, 50, 51, 52	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
54	53	expcomd 1462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
55	48, 54	sylbid 150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
56	55	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
57	45, 46, 56	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
58	57	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$
59	58	imp 124	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
60	59	impcom 125	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
61	44	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
62	61	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
63	43	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
64	63	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
65	46	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
66	62, 64, 65	3jca 1180	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
67	66	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
68	67	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		lesub1 8564	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
70	68, 69	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
71	60, 70	mpbid 147	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
72		swrdlend 11149	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ substr
73	42, 71, 72	sylc 62	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
74	26, 73	eqtrd 2240	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
75	74	ex 115	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
76		iffalse 3587	. . . . . . . . . . . . . . . . . . . . . 22
77	76	opeq1d 3839	. . . . . . . . . . . . . . . . . . . . 21
78	77	oveq2d 5983	. . . . . . . . . . . . . . . . . . . 20 substr substr
79		simplr 528	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ Word
80	79	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word
81		0zd 9419	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
82	34, 28, 35	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
83	82	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$
84	83	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
85	80, 81, 84	3jca 1180	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
86	61, 46	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
87	86	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
88		suble0 8584	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
89	87, 88	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$
90	89	biimpar 297	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
91		swrdlend 11149	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ substr
92	85, 90, 91	sylc 62	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
93	78, 92	sylan9eq 2260	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
94	93	ex 115	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
95	75, 94	jaoi 718	. . . . . . . . . . . . . . . . 17 $\/$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
96	22, 95	syl 14	. . . . . . . . . . . . . . . 16 DECID Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
97	21, 96	mpcom 36	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
98	12, 97	oveq12d 5985	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++
99		simpll 527	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ Word
100	14	nn0zd 9528	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$
101	34	ad2antrl 490	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$
102		swrdclg 11141	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$ substr Word
103	99, 100, 101, 102	syl3anc 1250	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ substr Word
104		ccatrid 11101	. . . . . . . . . . . . . . . 16 substr Word substr ++ substr
105	103, 104	syl 14	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ substr ++ substr
106	105	adantr 276	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr
107	98, 106	eqtrd 2240	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
108		iffalse 3587	. . . . . . . . . . . . . . . . . . 19
109	108	3ad2ant2 1022	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
110	109	opeq2d 3840	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
111	110	oveq2d 5983	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
112		simpl 109	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word Word
113	112, 30, 28	3anim123i 1187	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
114	113	3expb 1207	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
115		swrdlend 11149	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ substr
116	114, 115	syl 14	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ substr
117	116	imp 124	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
118	117	3adant2 1019	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
119	111, 118	eqtrd 2240	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
120	63, 46, 47	syl2an 289	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
121	120	biimprd 158	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
122	121	adantl 277	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
123	122	imp 124	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
124	123	3adant2 1019	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
125	124, 24	syl 14	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
126	125	oveq2d 5983	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
127	119, 126	oveq12d 5985	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr ++ substr
128		swrdclg 11141	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ substr Word
129		ccatlid 11100	. . . . . . . . . . . . . . . 16 substr Word ++ substr substr
130	41, 128, 129	3syl 17	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ ++ substr substr
131	130	3ad2ant1 1021	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ++ substr substr
132	127, 131	eqtrd 2240	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
133	108	3ad2ant2 1022	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
134	133	opeq2d 3840	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
135	134	oveq2d 5983	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
136	43, 46, 47	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
137	136	adantlr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
138	137	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$
139	138	biimpd 144	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
140	139	con3dimp 636	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
141	140	3adant2 1019	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
142	141, 76	syl 14	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
143	142	opeq1d 3839	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
144	143	oveq2d 5983	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
145	79	3ad2ant1 1021	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ Word
146		simplrr 536	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
147		simprlr 538	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
148	147	adantr 276	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
149		zltnle 9453	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
150	28, 34, 149	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
151		ltle 8195	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
152	46, 61, 151	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
153	150, 152	sylbird 170	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
154	153	adantl 277	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
155	154	imp 124	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
156		nn0sub2 9481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
157	146, 148, 155, 156	syl3anc 1250	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
158	157	3adant3 1020	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
159		pfxval 11165	. . . . . . . . . . . . . . . 16 Word $/\$ prefix substr
160	145, 158, 159	syl2anc 411	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ prefix substr
161	144, 160	eqtr4d 2243	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr prefix
162	135, 161	oveq12d 5985	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++ prefix
163	28	ad2antll 491	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$
164		zdcle 9484	. . . . . . . . . . . . . 14 $/\$ DECID
165	101, 163, 164	syl2anc 411	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ DECID
166	146	nn0zd 9528	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
167	100	adantr 276	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
168		zdcle 9484	. . . . . . . . . . . . . 14 $/\$ DECID
169	166, 167, 168	syl2anc 411	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ DECID
170	107, 132, 162, 165, 169	2if2dc 3619	. . . . . . . . . . . 12 Word $/\$ Word $/\$ $/\$ $/\$ substr ++ substr substr substr substr ++ prefix
171	170	exp32 365	. . . . . . . . . . 11 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ prefix
172	171	com12 30	. . . . . . . . . 10 $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ prefix
173	172	3adant3 1020	. . . . . . . . 9 $/\$ $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ prefix
174	8, 173	sylbi 121	. . . . . . . 8 Word $/\$ Word substr ++ substr substr substr substr ++ prefix
175	174	adantr 276	. . . . . . 7 $/\$ ♯ Word $/\$ Word substr ++ substr substr substr substr ++ prefix
176	175	com13 80	. . . . . 6 Word $/\$ Word $/\$ ♯ substr ++ substr substr substr substr ++ prefix
177	7, 176	sylbi 121	. . . . 5 ♯ Word $/\$ Word $/\$ ♯ substr ++ substr substr substr substr ++ prefix
178	5, 177	mpcom 36	. . . 4 Word $/\$ Word $/\$ ♯ substr ++ substr substr substr substr ++ prefix
179	178	imp 124	. . 3 Word $/\$ Word $/\$ $/\$ ♯ substr ++ substr substr substr substr ++ prefix
180	3, 179	eqtr4d 2243	. 2 Word $/\$ Word $/\$ $/\$ ♯ ++ substr substr ++ substr
181	180	ex 115	1 Word $/\$ Word $/\$ ♯ ++ substr substr ++ substr

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 710 DECID wdc 836 $/\$ w3a 981

wceq 1373

wcel 2178

c0 3468

cif 3579

cop 3646 class class class wbr 4059

cfv 5290 (class class class)co 5967

cr 7959

cc0 7960

caddc 7963

clt 8142

cle 8143

cmin 8278

cn0 9330

cz 9407

cfz 10165 ♯chash 10957 Word cword 11031 ++ cconcat 11084 substr csubstr 11136 prefix cpfx 11163

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2180 ax-14 2181 ax-ext 2189 ax-coll 4175 ax-sep 4178 ax-nul 4186 ax-pow 4234 ax-pr 4269 ax-un 4498 ax-setind 4603 ax-iinf 4654 ax-cnex 8051 ax-resscn 8052 ax-1cn 8053 ax-1re 8054 ax-icn 8055 ax-addcl 8056 ax-addrcl 8057 ax-mulcl 8058 ax-addcom 8060 ax-addass 8062 ax-distr 8064 ax-i2m1 8065 ax-0lt1 8066 ax-0id 8068 ax-rnegex 8069 ax-cnre 8071 ax-pre-ltirr 8072 ax-pre-ltwlin 8073 ax-pre-lttrn 8074 ax-pre-apti 8075 ax-pre-ltadd 8076

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-nel 2474 df-ral 2491 df-rex 2492 df-reu 2493 df-rab 2495 df-v 2778 df-sbc 3006 df-csb 3102 df-dif 3176 df-un 3178 df-in 3180 df-ss 3187 df-nul 3469 df-if 3580 df-pw 3628 df-sn 3649 df-pr 3650 df-op 3652 df-uni 3865 df-int 3900 df-iun 3943 df-br 4060 df-opab 4122 df-mpt 4123 df-tr 4159 df-id 4358 df-iord 4431 df-on 4433 df-ilim 4434 df-suc 4436 df-iom 4657 df-xp 4699 df-rel 4700 df-cnv 4701 df-co 4702 df-dm 4703 df-rn 4704 df-res 4705 df-ima 4706 df-iota 5251 df-fun 5292 df-fn 5293 df-f 5294 df-f1 5295 df-fo 5296 df-f1o 5297 df-fv 5298 df-riota 5922 df-ov 5970 df-oprab 5971 df-mpo 5972 df-1st 6249 df-2nd 6250 df-recs 6414 df-frec 6500 df-1o 6525 df-er 6643 df-en 6851 df-dom 6852 df-fin 6853 df-pnf 8144 df-mnf 8145 df-xr 8146 df-ltxr 8147 df-le 8148 df-sub 8280 df-neg 8281 df-inn 9072 df-n0 9331 df-z 9408 df-uz 9684 df-fz 10166 df-fzo 10300 df-ihash 10958 df-word 11032 df-concat 11085 df-substr 11137 df-pfx 11164

This theorem is referenced by: (None)

W3C validator