efgcpbllemb - Metamath Proof Explorer

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

Theorem efgcpbllemb 17483

Description: Lemma for efgrelex 17479. 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 17452	. 2 $/\$
6		efgcpbllem.1	. . . . . . 7 $/\$ ++ ++ ++ ++
7	6	relopabi 4964	. . . . . 6
8	7	a1i 11	. . . . 5 $/\$
9		efgred.d	. . . . . . . . 9 $\$
10		efgred.s	. . . . . . . . 9 Word $\$ $/\$ ..^
11	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17482	. . . . . . . 8 $/\$ $/\$ ++ ++ ++ ++
12	11	simp2bi 1046	. . . . . . 7
13	12	adantl 473	. . . . . 6 $/\$ $/\$
14	11	simp1bi 1045	. . . . . . 7
15	14	adantl 473	. . . . . 6 $/\$ $/\$
16	1, 2	efger 17446	. . . . . . . 8
17	16	a1i 11	. . . . . . 7 $/\$ $/\$
18	11	simp3bi 1047	. . . . . . . 8 ++ ++ ++ ++
19	18	adantl 473	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++
20	17, 19	ersym 7393	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
21	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17482	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
22	13, 15, 20, 21	syl3anbrc 1214	. . . . 5 $/\$ $/\$
23	14	ad2antrl 742	. . . . . 6 $/\$ $/\$ $/\$
24	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17482	. . . . . . . 8 $/\$ $/\$ ++ ++ ++ ++
25	24	simp2bi 1046	. . . . . . 7
26	25	ad2antll 743	. . . . . 6 $/\$ $/\$ $/\$
27	16	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$
28	18	ad2antrl 742	. . . . . . 7 $/\$ $/\$ $/\$ ++ ++ ++ ++
29	24	simp3bi 1047	. . . . . . . 8 ++ ++ ++ ++
30	29	ad2antll 743	. . . . . . 7 $/\$ $/\$ $/\$ ++ ++ ++ ++
31	27, 28, 30	ertrd 7397	. . . . . 6 $/\$ $/\$ $/\$ ++ ++ ++ ++
32	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17482	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
33	23, 26, 31, 32	syl3anbrc 1214	. . . . 5 $/\$ $/\$ $/\$
34	16	a1i 11	. . . . . . . . 9 $/\$ $/\$
35		fviss 5938	. . . . . . . . . . . . . 14 Word Word
36	1, 35	eqsstri 3448	. . . . . . . . . . . . 13 Word
37		simpll 768	. . . . . . . . . . . . 13 $/\$ $/\$
38	36, 37	sseldi 3416	. . . . . . . . . . . 12 $/\$ $/\$ Word
39		simpr 468	. . . . . . . . . . . . 13 $/\$ $/\$
40	36, 39	sseldi 3416	. . . . . . . . . . . 12 $/\$ $/\$ Word
41		ccatcl 12771	. . . . . . . . . . . 12 Word $/\$ Word ++ Word
42	38, 40, 41	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ ++ Word
43		simplr 770	. . . . . . . . . . . 12 $/\$ $/\$
44	36, 43	sseldi 3416	. . . . . . . . . . 11 $/\$ $/\$ Word
45		ccatcl 12771	. . . . . . . . . . 11 ++ Word $/\$ Word ++ ++ Word
46	42, 44, 45	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ ++ ++ Word
47	1	efgrcl 17443	. . . . . . . . . . . 12 $/\$ Word
48	47	simprd 470	. . . . . . . . . . 11 Word
49	48	ad2antrr 740	. . . . . . . . . 10 $/\$ $/\$ Word
50	46, 49	eleqtrrd 2552	. . . . . . . . 9 $/\$ $/\$ ++ ++
51	34, 50	erref 7401	. . . . . . . 8 $/\$ $/\$ ++ ++ ++ ++
52	51	ex 441	. . . . . . 7 $/\$ ++ ++ ++ ++
53	52	pm4.71d 646	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
54	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17482	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++
55		df-3an 1009	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++ $/\$ $/\$ ++ ++ ++ ++
56		anidm 656	. . . . . . . 8 $/\$
57	56	anbi1i 709	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++ $/\$ ++ ++ ++ ++
58	54, 55, 57	3bitri 279	. . . . . 6 $/\$ ++ ++ ++ ++
59	53, 58	syl6bbr 271	. . . . 5 $/\$
60	8, 22, 33, 59	iserd 7407	. . . 4 $/\$
61	1, 2, 3, 4	efgtf 17450	. . . . . . . . . 10 splice $/\$
62	61	simprd 470	. . . . . . . . 9
63	62	adantl 473	. . . . . . . 8 $/\$ $/\$
64		ffn 5739	. . . . . . . 8
65		ovelrn 6464	. . . . . . . 8
66	63, 64, 65	3syl 18	. . . . . . 7 $/\$ $/\$
67		simplr 770	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
68	62	ad2antlr 741	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
69		simprl 772	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
70		simprr 774	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
71	68, 69, 70	fovrnd 6460	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
72	50	adantr 472	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ ++ ++
73	37	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
74	36, 73	sseldi 3416	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Word
75	40	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Word
76		swrdcl 12829	. . . . . . . . . . . . . . . . 17 Word substr Word
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr Word
78		ccatcl 12771	. . . . . . . . . . . . . . . 16 Word $/\$ substr Word ++ substr Word
79	74, 77, 78	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr Word
80	3	efgmf 17441	. . . . . . . . . . . . . . . . . 18
81	80	ffvelrni 6036	. . . . . . . . . . . . . . . . 17
82	81	ad2antll 743	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
83	70, 82	s2cld 13025	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Word
84		ccatcl 12771	. . . . . . . . . . . . . . 15 ++ substr Word $/\$ Word ++ substr ++ Word
85	79, 83, 84	syl2anc 673	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ substr ++ Word
86		swrdcl 12829	. . . . . . . . . . . . . . 15 Word substr Word
87	75, 86	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ substr Word
88	44	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Word
89		ccatass 12783	. . . . . . . . . . . . . 14 ++ substr ++ Word $/\$ substr Word $/\$ Word ++ substr ++ ++ substr ++ ++ substr ++ ++ substr ++
90	85, 87, 88, 89	syl3anc 1292	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ ++ substr ++ ++ substr ++
91		ccatcl 12771	. . . . . . . . . . . . . . . . 17 substr Word $/\$ Word substr ++ Word
92	77, 83, 91	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr ++ Word
93		ccatass 12783	. . . . . . . . . . . . . . . 16 Word $/\$ substr ++ Word $/\$ substr Word ++ substr ++ ++ substr ++ substr ++ ++ substr
94	74, 92, 87, 93	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ substr ++ ++ substr
95		ccatass 12783	. . . . . . . . . . . . . . . . 17 Word $/\$ substr Word $/\$ Word ++ substr ++ ++ substr ++
96	74, 77, 83, 95	syl3anc 1292	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++
97	96	oveq1d 6323	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ substr ++ ++ substr
98	1, 2, 3, 4	efgtval 17451	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ splice
99	67, 69, 70, 98	syl3anc 1292	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ splice
100		splval 12912	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ Word splice substr ++ ++ substr
101	67, 69, 69, 83, 100	syl13anc 1294	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ splice substr ++ ++ substr
102	99, 101	eqtrd 2505	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr ++ ++ substr
103	102	oveq2d 6324	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ ++ substr ++ ++ substr
104	94, 97, 103	3eqtr4rd 2516	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ ++ substr ++ ++ substr
105	104	oveq1d 6323	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ substr ++ ++ substr ++
106		lencl 12737	. . . . . . . . . . . . . . . . . . 19 Word
107	74, 106	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
108		nn0uz 11217	. . . . . . . . . . . . . . . . . 18
109	107, 108	syl6eleq 2559	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
110		elfznn0 11913	. . . . . . . . . . . . . . . . . 18
111	110	ad2antrl 742	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
112		uzaddcl 11238	. . . . . . . . . . . . . . . . 17 $/\$
113	109, 111, 112	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
114	42	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++ Word
115		ccatlen 12772	. . . . . . . . . . . . . . . . . 18 ++ Word $/\$ Word ++ ++ ++
116	114, 88, 115	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++ ++ ++
117		ccatlen 12772	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word ++
118	74, 75, 117	syl2anc 673	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ ++
119		elfzuz3 11823	. . . . . . . . . . . . . . . . . . . . . 22
120	119	ad2antrl 742	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
121	107	nn0zd 11061	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
122		eluzadd 11211	. . . . . . . . . . . . . . . . . . . . 21 $/\$
123	120, 121, 122	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
124		lencl 12737	. . . . . . . . . . . . . . . . . . . . . . 23 Word
125	75, 124	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
126	125	nn0cnd 10951	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
127	107	nn0cnd 10951	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
128	126, 127	addcomd 9853	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
129	111	nn0cnd 10951	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
130	129, 127	addcomd 9853	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
131	130	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
132	123, 128, 131	3eltr3d 2563	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
133	118, 132	eqeltrd 2549	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++
134		lencl 12737	. . . . . . . . . . . . . . . . . . 19 Word
135	88, 134	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
136		uzaddcl 11238	. . . . . . . . . . . . . . . . . 18 ++ $/\$ ++
137	133, 135, 136	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++
138	116, 137	eqeltrd 2549	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ ++
139		elfzuzb 11820	. . . . . . . . . . . . . . . 16 ++ ++ $/\$ ++ ++
140	113, 138, 139	sylanbrc 677	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ ++
141	1, 2, 3, 4	efgtval 17451	. . . . . . . . . . . . . . 15 ++ ++ $/\$ ++ ++ $/\$ ++ ++ ++ ++ splice
142	72, 140, 70, 141	syl3anc 1292	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++ splice
143		wrd0 12742	. . . . . . . . . . . . . . . 16 Word
144	143	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Word
145		ccatcl 12771	. . . . . . . . . . . . . . . 16 substr Word $/\$ Word substr ++ Word
146	87, 88, 145	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ substr ++ Word
147		ccatrid 12782	. . . . . . . . . . . . . . . . . 18 ++ substr Word ++ substr ++ ++ substr
148	79, 147	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr
149	148	oveq1d 6323	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ ++ substr ++ substr ++
150		ccatass 12783	. . . . . . . . . . . . . . . . 17 ++ substr Word $/\$ substr Word $/\$ Word ++ substr ++ substr ++ ++ substr ++ substr ++
151	79, 87, 88, 150	syl3anc 1292	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++ ++ substr ++ substr ++
152		ccatass 12783	. . . . . . . . . . . . . . . . . . 19 Word $/\$ substr Word $/\$ substr Word ++ substr ++ substr ++ substr ++ substr
153	74, 77, 87, 152	syl3anc 1292	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++ substr ++ substr
154	111, 108	syl6eleq 2559	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
155		eluzfz1 11832	. . . . . . . . . . . . . . . . . . . . . 22
156	154, 155	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
157	125, 108	syl6eleq 2559	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
158		eluzfz2 11833	. . . . . . . . . . . . . . . . . . . . . 22
159	157, 158	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
160		ccatswrd 12866	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ $/\$ substr ++ substr substr
161	75, 156, 69, 159, 160	syl13anc 1294	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
162		swrdid 12838	. . . . . . . . . . . . . . . . . . . . 21 Word substr
163	75, 162	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ substr
164	161, 163	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ substr ++ substr
165	164	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++
166	153, 165	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++
167	166	oveq1d 6323	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++ ++ ++
168	149, 151, 167	3eqtr2rd 2512	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ substr ++ ++ substr ++
169		ccatlen 12772	. . . . . . . . . . . . . . . . 17 Word $/\$ substr Word ++ substr substr
170	74, 77, 169	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr substr
171		swrd0len 12832	. . . . . . . . . . . . . . . . . 18 Word $/\$ substr
172	75, 69, 171	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ substr
173	172	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr
174	170, 173	eqtr2d 2506	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr
175		hash0 12586	. . . . . . . . . . . . . . . . 17
176	175	oveq2i 6319	. . . . . . . . . . . . . . . 16
177	107, 111	nn0addcld 10953	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
178	177	nn0cnd 10951	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
179	178	addid1d 9851	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
180	176, 179	syl5req 2518	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
181	79, 144, 146, 83, 168, 174, 180	splval2 12918	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ ++ splice ++ substr ++ ++ substr ++
182	142, 181	eqtrd 2505	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ substr ++ ++ substr ++
183	90, 105, 182	3eqtr4d 2515	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
184	1, 2, 3, 4	efgtf 17450	. . . . . . . . . . . . . . 15 ++ ++ ++ ++ ++ ++ ++ ++ splice $/\$ ++ ++ ++ ++
185	184	simprd 470	. . . . . . . . . . . . . 14 ++ ++ ++ ++ ++ ++
186		ffn 5739	. . . . . . . . . . . . . 14 ++ ++ ++ ++ ++ ++ ++ ++
187	72, 185, 186	3syl 18	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
188		fnovrn 6463	. . . . . . . . . . . . 13 ++ ++ ++ ++ $/\$ ++ ++ $/\$ ++ ++ ++ ++
189	187, 140, 70, 188	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
190	183, 189	eqeltrd 2549	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
191	1, 2, 3, 4	efgi2 17453	. . . . . . . . . . 11 ++ ++ $/\$ ++ ++ ++ ++ ++ ++ ++ ++
192	72, 190, 191	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
193	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17482	. . . . . . . . . 10 $/\$ $/\$ ++ ++ ++ ++
194	67, 71, 192, 193	syl3anbrc 1214	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
195		vex 3034	. . . . . . . . . . 11
196		vex 3034	. . . . . . . . . . 11
197	195, 196	elec 7421	. . . . . . . . . 10
198		breq2 4399	. . . . . . . . . 10
199	197, 198	syl5bb 265	. . . . . . . . 9
200	194, 199	syl5ibrcom 230	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
201	200	rexlimdvva 2878	. . . . . . 7 $/\$ $/\$
202	66, 201	sylbid 223	. . . . . 6 $/\$ $/\$
203	202	ssrdv 3424	. . . . 5 $/\$ $/\$
204	203	ralrimiva 2809	. . . 4 $/\$
205		fvex 5889	. . . . . . 7 Word
206	1, 205	eqeltri 2545	. . . . . 6
207		erex 7405	. . . . . 6
208	60, 206, 207	mpisyl 21	. . . . 5 $/\$
209		ereq1 7388	. . . . . . 7
210		eceq2 7419	. . . . . . . . 9
211	210	sseq2d 3446	. . . . . . . 8
212	211	ralbidv 2829	. . . . . . 7
213	209, 212	anbi12d 725	. . . . . 6 $/\$ $/\$
214	213	elabg 3174	. . . . 5 $/\$ $/\$
215	208, 214	syl 17	. . . 4 $/\$ $/\$ $/\$
216	60, 204, 215	mpbir2and 936	. . 3 $/\$ $/\$
217		intss1 4241	. . 3 $/\$ $/\$
218	216, 217	syl 17	. 2 $/\$ $/\$
219	5, 218	syl5eqss 3462	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

cab 2457

wral 2756

wrex 2757

crab 2760

cvv 3031 $\$ cdif 3387

wss 3390

c0 3722

csn 3959

cpr 3961

cop 3965

cotp 3967

cint 4226

ciun 4269 class class class wbr 4395

copab 4453

cmpt 4454

cid 4749

cxp 4837

crn 4840

wrel 4844

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

cmpt2 6310

c1o 7193

c2o 7194

wer 7378

cec 7379

cc0 9557

c1 9558

caddc 9560

cmin 9880

cn0 10893

cz 10961

cuz 11182

cfz 11810 ..^cfzo 11942

chash 12553 Word cword 12703 ++ cconcat 12705 substr csubstr 12707 splice csplice 12708

cs2 12996 ~_FG cefg 17434

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-ot 3968 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-ec 7383 df-map 7492 df-pm 7493 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-2 10690 df-n0 10894 df-z 10962 df-uz 11183 df-fz 11811 df-fzo 11943 df-hash 12554 df-word 12711 df-concat 12713 df-s1 12714 df-substr 12715 df-splice 12716 df-s2 13003 df-efg 17437

This theorem is referenced by: efgcpbl 17484

W3C validator