swrdccat - Intuitionistic Logic Explorer

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

Theorem swrdccat 11262

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 11261	. . . 4 Word $/\$ Word $/\$ ♯ ++ substr substr substr substr ++ prefix
3	2	imp 124	. . 3 Word $/\$ Word $/\$ $/\$ ♯ ++ substr substr substr substr ++ prefix
4		lencl 11070	. . . . . 6 Word ♯
5	4	adantr 276	. . . . 5 Word $/\$ Word ♯
6	1	eqcomi 2233	. . . . . . 7 ♯
7	6	eleq1i 2295	. . . . . 6 ♯
8		elfz2nn0 10304	. . . . . . . . 9 $/\$ $/\$
9		iftrue 3607	. . . . . . . . . . . . . . . . . 18
10	9	adantl 277	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
11	10	opeq2d 3863	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
12	11	oveq2d 6016	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
13		0z 9453	. . . . . . . . . . . . . . . . 17
14		simprll 537	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
15	14	adantr 276	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
16	15	nn0zd 9563	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
17		simplrr 536	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
18	17	nn0zd 9563	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
19	16, 18	zsubcld 9570	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
20		zdcle 9519	. . . . . . . . . . . . . . . . 17 $/\$ DECID
21	13, 19, 20	sylancr 414	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ DECID
22		exmiddc 841	. . . . . . . . . . . . . . . . 17 DECID $\/$
23		iftrue 3607	. . . . . . . . . . . . . . . . . . . . . . 23
24	23	opeq1d 3862	. . . . . . . . . . . . . . . . . . . . . 22
25	24	oveq2d 6016	. . . . . . . . . . . . . . . . . . . . 21 substr substr
26	25	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
27		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word Word
28		nn0z 9462	. . . . . . . . . . . . . . . . . . . . . . . . 25
29		nn0z 9462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
30	29	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
31		zsubcl 9483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
32	30, 31	sylan 283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
33		nn0z 9462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
34	33	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35		zsubcl 9483	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1006	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ $/\$ Word $/\$ $/\$
41	39, 40	sylibr 134	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
42	41	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
43		nn0re 9374	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
44		nn0re 9374	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
45	43, 44	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
46		nn0re 9374	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47		subge0 8618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
48	47	adantlr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
49		simplr 528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
50		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
51		simpll 527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
52		letr 8225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
53	49, 50, 51, 52	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
54	53	expcomd 1484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1201	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
67	66	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
68	67	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		lesub1 8599	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
70	68, 69	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
71	60, 70	mpbid 147	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
72		swrdlend 11185	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ substr
73	42, 71, 72	sylc 62	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
74	26, 73	eqtrd 2262	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
75	74	ex 115	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
76		iffalse 3610	. . . . . . . . . . . . . . . . . . . . . 22
77	76	opeq1d 3862	. . . . . . . . . . . . . . . . . . . . 21
78	77	oveq2d 6016	. . . . . . . . . . . . . . . . . . . 20 substr substr
79		simplr 528	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ Word
80	79	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word
81		0zd 9454	. . . . . . . . . . . . . . . . . . . . . 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 1201	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
86	61, 46	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
87	86	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
88		suble0 8619	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
89	87, 88	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$
90	89	biimpar 297	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
91		swrdlend 11185	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ substr
92	85, 90, 91	sylc 62	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
93	78, 92	sylan9eq 2282	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
94	93	ex 115	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
95	75, 94	jaoi 721	. . . . . . . . . . . . . . . . 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 6018	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++
99		simpll 527	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ Word
100	14	nn0zd 9563	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$
101	34	ad2antrl 490	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$
102		swrdclg 11177	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$ substr Word
103	99, 100, 101, 102	syl3anc 1271	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ substr Word
104		ccatrid 11137	. . . . . . . . . . . . . . . 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 2262	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
108		iffalse 3610	. . . . . . . . . . . . . . . . . . 19
109	108	3ad2ant2 1043	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
110	109	opeq2d 3863	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
111	110	oveq2d 6016	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
112		simpl 109	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word Word
113	112, 30, 28	3anim123i 1208	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
114	113	3expb 1228	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
115		swrdlend 11185	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ substr
116	114, 115	syl 14	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ substr
117	116	imp 124	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
118	117	3adant2 1040	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
119	111, 118	eqtrd 2262	. . . . . . . . . . . . . . 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 1040	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
125	124, 24	syl 14	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
126	125	oveq2d 6016	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
127	119, 126	oveq12d 6018	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr ++ substr
128		swrdclg 11177	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ substr Word
129		ccatlid 11136	. . . . . . . . . . . . . . . 16 substr Word ++ substr substr
130	41, 128, 129	3syl 17	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ ++ substr substr
131	130	3ad2ant1 1042	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ++ substr substr
132	127, 131	eqtrd 2262	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
133	108	3ad2ant2 1043	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
134	133	opeq2d 3863	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
135	134	oveq2d 6016	. . . . . . . . . . . . . 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 638	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
141	140	3adant2 1040	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
142	141, 76	syl 14	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
143	142	opeq1d 3862	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
144	143	oveq2d 6016	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
145	79	3ad2ant1 1042	. . . . . . . . . . . . . . . 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 9488	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
150	28, 34, 149	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
151		ltle 8230	. . . . . . . . . . . . . . . . . . . . . 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 9516	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
157	146, 148, 155, 156	syl3anc 1271	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
158	157	3adant3 1041	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
159		pfxval 11201	. . . . . . . . . . . . . . . 16 Word $/\$ prefix substr
160	145, 158, 159	syl2anc 411	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ prefix substr
161	144, 160	eqtr4d 2265	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr prefix
162	135, 161	oveq12d 6018	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++ prefix
163	28	ad2antll 491	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$
164		zdcle 9519	. . . . . . . . . . . . . 14 $/\$ DECID
165	101, 163, 164	syl2anc 411	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ DECID
166	146	nn0zd 9563	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
167	100	adantr 276	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
168		zdcle 9519	. . . . . . . . . . . . . 14 $/\$ DECID
169	166, 167, 168	syl2anc 411	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ DECID
170	107, 132, 162, 165, 169	2if2dc 3642	. . . . . . . . . . . 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 1041	. . . . . . . . 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 2265	. 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 713 DECID wdc 839 $/\$ w3a 1002

wceq 1395

wcel 2200

c0 3491

cif 3602

cop 3669 class class class wbr 4082

cfv 5317 (class class class)co 6000

cr 7994

cc0 7995

caddc 7998

clt 8177

cle 8178

cmin 8313

cn0 9365

cz 9442

cfz 10200 ♯chash 10992 Word cword 11066 ++ cconcat 11120 substr csubstr 11172 prefix cpfx 11199

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4523 ax-setind 4628 ax-iinf 4679 ax-cnex 8086 ax-resscn 8087 ax-1cn 8088 ax-1re 8089 ax-icn 8090 ax-addcl 8091 ax-addrcl 8092 ax-mulcl 8093 ax-addcom 8095 ax-addass 8097 ax-distr 8099 ax-i2m1 8100 ax-0lt1 8101 ax-0id 8103 ax-rnegex 8104 ax-cnre 8106 ax-pre-ltirr 8107 ax-pre-ltwlin 8108 ax-pre-lttrn 8109 ax-pre-apti 8110 ax-pre-ltadd 8111

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4383 df-iord 4456 df-on 4458 df-ilim 4459 df-suc 4461 df-iom 4682 df-xp 4724 df-rel 4725 df-cnv 4726 df-co 4727 df-dm 4728 df-rn 4729 df-res 4730 df-ima 4731 df-iota 5277 df-fun 5319 df-fn 5320 df-f 5321 df-f1 5322 df-fo 5323 df-f1o 5324 df-fv 5325 df-riota 5953 df-ov 6003 df-oprab 6004 df-mpo 6005 df-1st 6284 df-2nd 6285 df-recs 6449 df-frec 6535 df-1o 6560 df-er 6678 df-en 6886 df-dom 6887 df-fin 6888 df-pnf 8179 df-mnf 8180 df-xr 8181 df-ltxr 8182 df-le 8183 df-sub 8315 df-neg 8316 df-inn 9107 df-n0 9366 df-z 9443 df-uz 9719 df-fz 10201 df-fzo 10335 df-ihash 10993 df-word 11067 df-concat 11121 df-substr 11173 df-pfx 11200

This theorem is referenced by: (None)

W3C validator