efgcpbllemb - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > efgcpbllemb		Structured version Unicode version

Theorem efgcpbllemb 17393

Description: Lemma for efgrelex 17389. Show that

is an equivalence relation containing all direct extensions of a word, so is closed under

. (Contributed by Mario Carneiro, 1-Oct-2015.)

**Hypotheses**
Ref	Expression
efgval.w	Word
efgval.r	~_FG
efgval2.m	$\$
efgval2.t	splice
efgred.d	$\$
efgred.s	Word $\$ $/\$ ..^
efgcpbllem.1	$/\$ ++ ++ ++ ++

**Assertion**
Ref	Expression
efgcpbllemb	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem efgcpbllemb Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		efgval.w	. . 3 Word
2		efgval.r	. . 3 ~_FG
3		efgval2.m	. . 3 $\$
4		efgval2.t	. . 3 splice
5	1, 2, 3, 4	efgval2 17362	. 2 $/\$
6		efgcpbllem.1	. . . . . . 7 $/\$ ++ ++ ++ ++
7	6	relopabi 4975	. . . . . 6
8	7	a1i 11	. . . . 5 $/\$
9		efgred.d	. . . . . . . . 9 $\$
10		efgred.s	. . . . . . . . 9 Word $\$ $/\$ ..^
11	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17392	. . . . . . . 8 $/\$ $/\$ ++ ++ ++ ++
12	11	simp2bi 1021	. . . . . . 7
13	12	adantl 467	. . . . . 6 $/\$ $/\$
14	11	simp1bi 1020	. . . . . . 7
15	14	adantl 467	. . . . . 6 $/\$ $/\$
16	1, 2	efger 17356	. . . . . . . 8
17	16	a1i 11	. . . . . . 7 $/\$ $/\$
18	11	simp3bi 1022	. . . . . . . 8 ++ ++ ++ ++
19	18	adantl 467	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++
20	17, 19	ersym 7380	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
21	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17392	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
22	13, 15, 20, 21	syl3anbrc 1189	. . . . 5 $/\$ $/\$
23	14	ad2antrl 732	. . . . . 6 $/\$ $/\$ $/\$
24	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17392	. . . . . . . 8 $/\$ $/\$ ++ ++ ++ ++
25	24	simp2bi 1021	. . . . . . 7
26	25	ad2antll 733	. . . . . 6 $/\$ $/\$ $/\$
27	16	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$
28	18	ad2antrl 732	. . . . . . 7 $/\$ $/\$ $/\$ ++ ++ ++ ++
29	24	simp3bi 1022	. . . . . . . 8 ++ ++ ++ ++
30	29	ad2antll 733	. . . . . . 7 $/\$ $/\$ $/\$ ++ ++ ++ ++
31	27, 28, 30	ertrd 7384	. . . . . 6 $/\$ $/\$ $/\$ ++ ++ ++ ++
32	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17392	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
33	23, 26, 31, 32	syl3anbrc 1189	. . . . 5 $/\$ $/\$ $/\$
34	16	a1i 11	. . . . . . . . 9 $/\$ $/\$
35		fviss 5936	. . . . . . . . . . . . . 14 Word Word
36	1, 35	eqsstri 3494	. . . . . . . . . . . . 13 Word
37		simpll 758	. . . . . . . . . . . . 13 $/\$ $/\$
38	36, 37	sseldi 3462	. . . . . . . . . . . 12 $/\$ $/\$ Word
39		simpr 462	. . . . . . . . . . . . 13 $/\$ $/\$
40	36, 39	sseldi 3462	. . . . . . . . . . . 12 $/\$ $/\$ Word
41		ccatcl 12713	. . . . . . . . . . . 12 Word $/\$ Word ++ Word
42	38, 40, 41	syl2anc 665	. . . . . . . . . . 11 $/\$ $/\$ ++ Word
43		simplr 760	. . . . . . . . . . . 12 $/\$ $/\$
44	36, 43	sseldi 3462	. . . . . . . . . . 11 $/\$ $/\$ Word
45		ccatcl 12713	. . . . . . . . . . 11 ++ Word $/\$ Word ++ ++ Word
46	42, 44, 45	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ ++ ++ Word
47	1	efgrcl 17353	. . . . . . . . . . . 12 $/\$ Word
48	47	simprd 464	. . . . . . . . . . 11 Word
49	48	ad2antrr 730	. . . . . . . . . 10 $/\$ $/\$ Word
50	46, 49	eleqtrrd 2513	. . . . . . . . 9 $/\$ $/\$ ++ ++
51	34, 50	erref 7388	. . . . . . . 8 $/\$ $/\$ ++ ++ ++ ++
52	51	ex 435	. . . . . . 7 $/\$ ++ ++ ++ ++
53	52	pm4.71d 638	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
54	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17392	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++
55		df-3an 984	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++ $/\$ $/\$ ++ ++ ++ ++
56		anidm 648	. . . . . . . 8 $/\$
57	56	anbi1i 699	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++ $/\$ ++ ++ ++ ++
58	54, 55, 57	3bitri 274	. . . . . 6 $/\$ ++ ++ ++ ++
59	53, 58	syl6bbr 266	. . . . 5 $/\$
60	8, 22, 33, 59	iserd 7394	. . . 4 $/\$
61	1, 2, 3, 4	efgtf 17360	. . . . . . . . . 10 splice $/\$
62	61	simprd 464	. . . . . . . . 9
63	62	adantl 467	. . . . . . . 8 $/\$ $/\$
64		ffn 5743	. . . . . . . 8
65		ovelrn 6456	. . . . . . . 8
66	63, 64, 65	3syl 18	. . . . . . 7 $/\$ $/\$
67		simplr 760	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
68	62	ad2antlr 731	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
69		simprl 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
70		simprr 764	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
71	68, 69, 70	fovrnd 6452	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
72	50	adantr 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ ++ ++
73	37	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
74	36, 73	sseldi 3462	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Word
75	40	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Word
76		swrdcl 12766	. . . . . . . . . . . . . . . . 17 Word substr Word
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr Word
78		ccatcl 12713	. . . . . . . . . . . . . . . 16 Word $/\$ substr Word ++ substr Word
79	74, 77, 78	syl2anc 665	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr Word
80	3	efgmf 17351	. . . . . . . . . . . . . . . . . 18
81	80	ffvelrni 6033	. . . . . . . . . . . . . . . . 17
82	81	ad2antll 733	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
83	70, 82	s2cld 12956	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Word
84		ccatcl 12713	. . . . . . . . . . . . . . 15 ++ substr Word $/\$ Word ++ substr ++ Word
85	79, 83, 84	syl2anc 665	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ substr ++ Word
86		swrdcl 12766	. . . . . . . . . . . . . . 15 Word substr Word
87	75, 86	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ substr Word
88	44	adantr 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Word
89		ccatass 12725	. . . . . . . . . . . . . 14 ++ substr ++ Word $/\$ substr Word $/\$ Word ++ substr ++ ++ substr ++ ++ substr ++ ++ substr ++
90	85, 87, 88, 89	syl3anc 1264	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ ++ substr ++ ++ substr ++
91		ccatcl 12713	. . . . . . . . . . . . . . . . 17 substr Word $/\$ Word substr ++ Word
92	77, 83, 91	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr ++ Word
93		ccatass 12725	. . . . . . . . . . . . . . . 16 Word $/\$ substr ++ Word $/\$ substr Word ++ substr ++ ++ substr ++ substr ++ ++ substr
94	74, 92, 87, 93	syl3anc 1264	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ substr ++ ++ substr
95		ccatass 12725	. . . . . . . . . . . . . . . . 17 Word $/\$ substr Word $/\$ Word ++ substr ++ ++ substr ++
96	74, 77, 83, 95	syl3anc 1264	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++
97	96	oveq1d 6317	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ substr ++ ++ substr
98	1, 2, 3, 4	efgtval 17361	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ splice
99	67, 69, 70, 98	syl3anc 1264	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ splice
100		splval 12849	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ Word splice substr ++ ++ substr
101	67, 69, 69, 83, 100	syl13anc 1266	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ splice substr ++ ++ substr
102	99, 101	eqtrd 2463	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr ++ ++ substr
103	102	oveq2d 6318	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ ++ substr ++ ++ substr
104	94, 97, 103	3eqtr4rd 2474	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ ++ substr ++ ++ substr
105	104	oveq1d 6317	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ substr ++ ++ substr ++
106		lencl 12680	. . . . . . . . . . . . . . . . . . 19 Word
107	74, 106	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
108		nn0uz 11194	. . . . . . . . . . . . . . . . . 18
109	107, 108	syl6eleq 2520	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
110		elfznn0 11888	. . . . . . . . . . . . . . . . . 18
111	110	ad2antrl 732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
112		uzaddcl 11216	. . . . . . . . . . . . . . . . 17 $/\$
113	109, 111, 112	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
114	42	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++ Word
115		ccatlen 12714	. . . . . . . . . . . . . . . . . 18 ++ Word $/\$ Word ++ ++ ++
116	114, 88, 115	syl2anc 665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++ ++ ++
117		ccatlen 12714	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word ++
118	74, 75, 117	syl2anc 665	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ ++
119		elfzuz3 11798	. . . . . . . . . . . . . . . . . . . . . 22
120	119	ad2antrl 732	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
121	107	nn0zd 11039	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
122		eluzadd 11188	. . . . . . . . . . . . . . . . . . . . 21 $/\$
123	120, 121, 122	syl2anc 665	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
124		lencl 12680	. . . . . . . . . . . . . . . . . . . . . . 23 Word
125	75, 124	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
126	125	nn0cnd 10928	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
127	107	nn0cnd 10928	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
128	126, 127	addcomd 9836	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
129	111	nn0cnd 10928	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
130	129, 127	addcomd 9836	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
131	130	fveq2d 5882	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
132	123, 128, 131	3eltr3d 2524	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
133	118, 132	eqeltrd 2510	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++
134		lencl 12680	. . . . . . . . . . . . . . . . . . 19 Word
135	88, 134	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
136		uzaddcl 11216	. . . . . . . . . . . . . . . . . 18 ++ $/\$ ++
137	133, 135, 136	syl2anc 665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++
138	116, 137	eqeltrd 2510	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ ++
139		elfzuzb 11795	. . . . . . . . . . . . . . . 16 ++ ++ $/\$ ++ ++
140	113, 138, 139	sylanbrc 668	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ ++
141	1, 2, 3, 4	efgtval 17361	. . . . . . . . . . . . . . 15 ++ ++ $/\$ ++ ++ $/\$ ++ ++ ++ ++ splice
142	72, 140, 70, 141	syl3anc 1264	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++ splice
143		wrd0 12684	. . . . . . . . . . . . . . . 16 Word
144	143	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Word
145		ccatcl 12713	. . . . . . . . . . . . . . . 16 substr Word $/\$ Word substr ++ Word
146	87, 88, 145	syl2anc 665	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ substr ++ Word
147		ccatrid 12724	. . . . . . . . . . . . . . . . . 18 ++ substr Word ++ substr ++ ++ substr
148	79, 147	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr
149	148	oveq1d 6317	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ ++ substr ++ substr ++
150		ccatass 12725	. . . . . . . . . . . . . . . . 17 ++ substr Word $/\$ substr Word $/\$ Word ++ substr ++ substr ++ ++ substr ++ substr ++
151	79, 87, 88, 150	syl3anc 1264	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++ ++ substr ++ substr ++
152		ccatass 12725	. . . . . . . . . . . . . . . . . . 19 Word $/\$ substr Word $/\$ substr Word ++ substr ++ substr ++ substr ++ substr
153	74, 77, 87, 152	syl3anc 1264	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++ substr ++ substr
154	111, 108	syl6eleq 2520	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
155		eluzfz1 11807	. . . . . . . . . . . . . . . . . . . . . 22
156	154, 155	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
157	125, 108	syl6eleq 2520	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
158		eluzfz2 11808	. . . . . . . . . . . . . . . . . . . . . 22
159	157, 158	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
160		ccatswrd 12803	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ $/\$ substr ++ substr substr
161	75, 156, 69, 159, 160	syl13anc 1266	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
162		swrdid 12775	. . . . . . . . . . . . . . . . . . . . 21 Word substr
163	75, 162	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ substr
164	161, 163	eqtrd 2463	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ substr ++ substr
165	164	oveq2d 6318	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++
166	153, 165	eqtrd 2463	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++
167	166	oveq1d 6317	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++ ++ ++
168	149, 151, 167	3eqtr2rd 2470	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ substr ++ ++ substr ++
169		ccatlen 12714	. . . . . . . . . . . . . . . . 17 Word $/\$ substr Word ++ substr substr
170	74, 77, 169	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr substr
171		swrd0len 12769	. . . . . . . . . . . . . . . . . 18 Word $/\$ substr
172	75, 69, 171	syl2anc 665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ substr
173	172	oveq2d 6318	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr
174	170, 173	eqtr2d 2464	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr
175		hash0 12548	. . . . . . . . . . . . . . . . 17
176	175	oveq2i 6313	. . . . . . . . . . . . . . . 16
177	107, 111	nn0addcld 10930	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
178	177	nn0cnd 10928	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
179	178	addid1d 9834	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
180	176, 179	syl5req 2476	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
181	79, 144, 146, 83, 168, 174, 180	splval2 12855	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ ++ splice ++ substr ++ ++ substr ++
182	142, 181	eqtrd 2463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ substr ++ ++ substr ++
183	90, 105, 182	3eqtr4d 2473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
184	1, 2, 3, 4	efgtf 17360	. . . . . . . . . . . . . . 15 ++ ++ ++ ++ ++ ++ ++ ++ splice $/\$ ++ ++ ++ ++
185	184	simprd 464	. . . . . . . . . . . . . 14 ++ ++ ++ ++ ++ ++
186		ffn 5743	. . . . . . . . . . . . . 14 ++ ++ ++ ++ ++ ++ ++ ++
187	72, 185, 186	3syl 18	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
188		fnovrn 6455	. . . . . . . . . . . . 13 ++ ++ ++ ++ $/\$ ++ ++ $/\$ ++ ++ ++ ++
189	187, 140, 70, 188	syl3anc 1264	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
190	183, 189	eqeltrd 2510	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
191	1, 2, 3, 4	efgi2 17363	. . . . . . . . . . 11 ++ ++ $/\$ ++ ++ ++ ++ ++ ++ ++ ++
192	72, 190, 191	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
193	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17392	. . . . . . . . . 10 $/\$ $/\$ ++ ++ ++ ++
194	67, 71, 192, 193	syl3anbrc 1189	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
195		vex 3084	. . . . . . . . . . 11
196		vex 3084	. . . . . . . . . . 11
197	195, 196	elec 7408	. . . . . . . . . 10
198		breq2 4424	. . . . . . . . . 10
199	197, 198	syl5bb 260	. . . . . . . . 9
200	194, 199	syl5ibrcom 225	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
201	200	rexlimdvva 2924	. . . . . . 7 $/\$ $/\$
202	66, 201	sylbid 218	. . . . . 6 $/\$ $/\$
203	202	ssrdv 3470	. . . . 5 $/\$ $/\$
204	203	ralrimiva 2839	. . . 4 $/\$
205		fvex 5888	. . . . . . 7 Word
206	1, 205	eqeltri 2506	. . . . . 6
207		erex 7392	. . . . . 6
208	60, 206, 207	mpisyl 22	. . . . 5 $/\$
209		ereq1 7375	. . . . . . 7
210		eceq2 7406	. . . . . . . . 9
211	210	sseq2d 3492	. . . . . . . 8
212	211	ralbidv 2864	. . . . . . 7
213	209, 212	anbi12d 715	. . . . . 6 $/\$ $/\$
214	213	elabg 3219	. . . . 5 $/\$ $/\$
215	208, 214	syl 17	. . . 4 $/\$ $/\$ $/\$
216	60, 204, 215	mpbir2and 930	. . 3 $/\$ $/\$
217		intss1 4267	. . 3 $/\$ $/\$
218	216, 217	syl 17	. 2 $/\$ $/\$
219	5, 218	syl5eqss 3508	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1868

cab 2407

wral 2775

wrex 2776

crab 2779

cvv 3081 $\$ cdif 3433

wss 3436

c0 3761

csn 3996

cpr 3998

cop 4002

cotp 4004

cint 4252

ciun 4296 class class class wbr 4420

copab 4478

cmpt 4479

cid 4760

cxp 4848

crn 4851

wrel 4855

wfn 5593

wf 5594

cfv 5598 (class class class)co 6302

cmpt2 6304

c1o 7180

c2o 7181

wer 7365

cec 7366

cc0 9540

c1 9541

caddc 9543

cmin 9861

cn0 10870

cz 10938

cuz 11160

cfz 11785 ..^cfzo 11916

chash 12515 Word cword 12649 ++ cconcat 12651 substr csubstr 12653 splice csplice 12654

cs2 12928 ~_FG cefg 17344

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4552 ax-pow 4599 ax-pr 4657 ax-un 6594 ax-cnex 9596 ax-resscn 9597 ax-1cn 9598 ax-icn 9599 ax-addcl 9600 ax-addrcl 9601 ax-mulcl 9602 ax-mulrcl 9603 ax-mulcom 9604 ax-addass 9605 ax-mulass 9606 ax-distr 9607 ax-i2m1 9608 ax-1ne0 9609 ax-1rid 9610 ax-rnegex 9611 ax-rrecex 9612 ax-cnre 9613 ax-pre-lttri 9614 ax-pre-lttrn 9615 ax-pre-ltadd 9616 ax-pre-mulgt0 9617

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-nel 2621 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-ot 4005 df-uni 4217 df-int 4253 df-iun 4298 df-iin 4299 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4761 df-id 4765 df-po 4771 df-so 4772 df-fr 4809 df-we 4811 df-xp 4856 df-rel 4857 df-cnv 4858 df-co 4859 df-dm 4860 df-rn 4861 df-res 4862 df-ima 4863 df-pred 5396 df-ord 5442 df-on 5443 df-lim 5444 df-suc 5445 df-iota 5562 df-fun 5600 df-fn 5601 df-f 5602 df-f1 5603 df-fo 5604 df-f1o 5605 df-fv 5606 df-riota 6264 df-ov 6305 df-oprab 6306 df-mpt2 6307 df-om 6704 df-1st 6804 df-2nd 6805 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-2o 7188 df-oadd 7191 df-er 7368 df-ec 7370 df-map 7479 df-pm 7480 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-card 8375 df-cda 8599 df-pnf 9678 df-mnf 9679 df-xr 9680 df-ltxr 9681 df-le 9682 df-sub 9863 df-neg 9864 df-nn 10611 df-2 10669 df-n0 10871 df-z 10939 df-uz 11161 df-fz 11786 df-fzo 11917 df-hash 12516 df-word 12657 df-concat 12659 df-s1 12660 df-substr 12661 df-splice 12662 df-s2 12935 df-efg 17347

This theorem is referenced by: efgcpbl 17394

W3C validator