swrdccat - Intuitionistic Logic Explorer

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

Theorem swrdccat 11427

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 11426	. . . 4 Word $/\$ Word $/\$ ♯ ++ substr substr substr substr ++ prefix
3	2	imp 124	. . 3 Word $/\$ Word $/\$ $/\$ ♯ ++ substr substr substr substr ++ prefix
4		lencl 11228	. . . . . 6 Word ♯
5	4	adantr 276	. . . . 5 Word $/\$ Word ♯
6	1	eqcomi 2236	. . . . . . 7 ♯
7	6	eleq1i 2298	. . . . . 6 ♯
8		elfz2nn0 10446	. . . . . . . . 9 $/\$ $/\$
9		iftrue 3627	. . . . . . . . . . . . . . . . . 18
10	9	adantl 277	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
11	10	opeq2d 3890	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
12	11	oveq2d 6066	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
13		0z 9588	. . . . . . . . . . . . . . . . 17
14		simprll 539	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
15	14	adantr 276	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
16	15	nn0zd 9698	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
17		simplrr 538	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
18	17	nn0zd 9698	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
19	16, 18	zsubcld 9705	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
20		zdcle 9654	. . . . . . . . . . . . . . . . 17 $/\$ DECID
21	13, 19, 20	sylancr 414	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ DECID
22		exmiddc 844	. . . . . . . . . . . . . . . . 17 DECID $\/$
23		iftrue 3627	. . . . . . . . . . . . . . . . . . . . . . 23
24	23	opeq1d 3889	. . . . . . . . . . . . . . . . . . . . . 22
25	24	oveq2d 6066	. . . . . . . . . . . . . . . . . . . . 21 substr substr
26	25	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
27		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word Word
28		nn0z 9597	. . . . . . . . . . . . . . . . . . . . . . . . 25
29		nn0z 9597	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
30	29	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
31		zsubcl 9618	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
32	30, 31	sylan 283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
33		nn0z 9597	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
34	33	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35		zsubcl 9618	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1009	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ $/\$ Word $/\$ $/\$
41	39, 40	sylibr 134	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
42	41	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
43		nn0re 9505	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
44		nn0re 9505	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
45	43, 44	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
46		nn0re 9505	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47		subge0 8749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
48	47	adantlr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
49		simplr 529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
50		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
51		simpll 527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
52		letr 8356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
53	49, 50, 51, 52	syl3anc 1274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
54	53	expcomd 1487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1204	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
67	66	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
68	67	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		lesub1 8730	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
70	68, 69	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
71	60, 70	mpbid 147	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
72		swrdlend 11350	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ substr
73	42, 71, 72	sylc 62	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
74	26, 73	eqtrd 2265	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
75	74	ex 115	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
76		iffalse 3630	. . . . . . . . . . . . . . . . . . . . . 22
77	76	opeq1d 3889	. . . . . . . . . . . . . . . . . . . . 21
78	77	oveq2d 6066	. . . . . . . . . . . . . . . . . . . 20 substr substr
79		simplr 529	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ Word
80	79	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word
81		0zd 9589	. . . . . . . . . . . . . . . . . . . . . 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 1204	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
86	61, 46	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
87	86	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
88		suble0 8750	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
89	87, 88	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$
90	89	biimpar 297	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
91		swrdlend 11350	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ substr
92	85, 90, 91	sylc 62	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
93	78, 92	sylan9eq 2285	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
94	93	ex 115	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
95	75, 94	jaoi 724	. . . . . . . . . . . . . . . . 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 6068	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++
99		simpll 527	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ Word
100	14	nn0zd 9698	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$
101	34	ad2antrl 490	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$
102		swrdclg 11342	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$ substr Word
103	99, 100, 101, 102	syl3anc 1274	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ substr Word
104		ccatrid 11295	. . . . . . . . . . . . . . . 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 2265	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
108		iffalse 3630	. . . . . . . . . . . . . . . . . . 19
109	108	3ad2ant2 1046	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
110	109	opeq2d 3890	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
111	110	oveq2d 6066	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
112		simpl 109	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word Word
113	112, 30, 28	3anim123i 1211	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
114	113	3expb 1231	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
115		swrdlend 11350	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ substr
116	114, 115	syl 14	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ substr
117	116	imp 124	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
118	117	3adant2 1043	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
119	111, 118	eqtrd 2265	. . . . . . . . . . . . . . 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 1043	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
125	124, 24	syl 14	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
126	125	oveq2d 6066	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
127	119, 126	oveq12d 6068	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr ++ substr
128		swrdclg 11342	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ substr Word
129		ccatlid 11294	. . . . . . . . . . . . . . . 16 substr Word ++ substr substr
130	41, 128, 129	3syl 17	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ ++ substr substr
131	130	3ad2ant1 1045	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ++ substr substr
132	127, 131	eqtrd 2265	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
133	108	3ad2ant2 1046	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
134	133	opeq2d 3890	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
135	134	oveq2d 6066	. . . . . . . . . . . . . 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 640	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
141	140	3adant2 1043	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
142	141, 76	syl 14	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
143	142	opeq1d 3889	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
144	143	oveq2d 6066	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
145	79	3ad2ant1 1045	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ Word
146		simplrr 538	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
147		simprlr 540	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
148	147	adantr 276	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
149		zltnle 9623	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
150	28, 34, 149	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
151		ltle 8361	. . . . . . . . . . . . . . . . . . . . . 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 9651	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
157	146, 148, 155, 156	syl3anc 1274	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
158	157	3adant3 1044	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
159		pfxval 11366	. . . . . . . . . . . . . . . 16 Word $/\$ prefix substr
160	145, 158, 159	syl2anc 411	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ prefix substr
161	144, 160	eqtr4d 2268	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr prefix
162	135, 161	oveq12d 6068	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++ prefix
163	28	ad2antll 491	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$
164		zdcle 9654	. . . . . . . . . . . . . 14 $/\$ DECID
165	101, 163, 164	syl2anc 411	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ DECID
166	146	nn0zd 9698	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
167	100	adantr 276	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
168		zdcle 9654	. . . . . . . . . . . . . 14 $/\$ DECID
169	166, 167, 168	syl2anc 411	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ DECID
170	107, 132, 162, 165, 169	2if2dc 3662	. . . . . . . . . . . 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 1044	. . . . . . . . 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 2268	. 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 716 DECID wdc 842 $/\$ w3a 1005

wceq 1398

wcel 2203

c0 3508

cif 3620

cop 3692 class class class wbr 4109

cfv 5352 (class class class)co 6050

cr 8126

cc0 8127

caddc 8130

clt 8308

cle 8309

cmin 8444

cn0 9496

cz 9577

cfz 10342 ♯chash 11138 Word cword 11224 ++ cconcat 11278 substr csubstr 11337 prefix cpfx 11364

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-coll 4225 ax-sep 4228 ax-nul 4236 ax-pow 4287 ax-pr 4322 ax-un 4554 ax-setind 4659 ax-iinf 4710 ax-cnex 8218 ax-resscn 8219 ax-1cn 8220 ax-1re 8221 ax-icn 8222 ax-addcl 8223 ax-addrcl 8224 ax-mulcl 8225 ax-addcom 8227 ax-addass 8229 ax-distr 8231 ax-i2m1 8232 ax-0lt1 8233 ax-0id 8235 ax-rnegex 8236 ax-cnre 8238 ax-pre-ltirr 8239 ax-pre-ltwlin 8240 ax-pre-lttrn 8241 ax-pre-apti 8242 ax-pre-ltadd 8243

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-reu 2527 df-rab 2529 df-v 2815 df-sbc 3043 df-csb 3139 df-dif 3213 df-un 3215 df-in 3217 df-ss 3224 df-nul 3509 df-if 3621 df-pw 3671 df-sn 3695 df-pr 3696 df-op 3698 df-uni 3915 df-int 3950 df-iun 3993 df-br 4110 df-opab 4172 df-mpt 4173 df-tr 4209 df-id 4414 df-iord 4487 df-on 4489 df-ilim 4490 df-suc 4492 df-iom 4713 df-xp 4755 df-rel 4756 df-cnv 4757 df-co 4758 df-dm 4759 df-rn 4760 df-res 4761 df-ima 4762 df-iota 5312 df-fun 5354 df-fn 5355 df-f 5356 df-f1 5357 df-fo 5358 df-f1o 5359 df-fv 5360 df-riota 6003 df-ov 6053 df-oprab 6054 df-mpo 6055 df-1st 6334 df-2nd 6335 df-recs 6536 df-frec 6622 df-1o 6647 df-er 6767 df-en 6976 df-dom 6977 df-fin 6978 df-pnf 8310 df-mnf 8311 df-xr 8312 df-ltxr 8313 df-le 8314 df-sub 8446 df-neg 8447 df-inn 9238 df-n0 9497 df-z 9578 df-uz 9854 df-fz 10343 df-fzo 10477 df-ihash 11139 df-word 11225 df-concat 11279 df-substr 11338 df-pfx 11365

This theorem is referenced by: (None)

W3C validator