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 17405

Description: Lemma for efgrelex 17401. 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 17374	. 2 $/\$
6		efgcpbllem.1	. . . . . . 7 $/\$ ++ ++ ++ ++
7	6	relopabi 4959	. . . . . 6
8	7	a1i 11	. . . . 5 $/\$
9		efgred.d	. . . . . . . . 9 $\$
10		efgred.s	. . . . . . . . 9 Word $\$ $/\$ ..^
11	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17404	. . . . . . . 8 $/\$ $/\$ ++ ++ ++ ++
12	11	simp2bi 1024	. . . . . . 7
13	12	adantl 468	. . . . . 6 $/\$ $/\$
14	11	simp1bi 1023	. . . . . . 7
15	14	adantl 468	. . . . . 6 $/\$ $/\$
16	1, 2	efger 17368	. . . . . . . 8
17	16	a1i 11	. . . . . . 7 $/\$ $/\$
18	11	simp3bi 1025	. . . . . . . 8 ++ ++ ++ ++
19	18	adantl 468	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++
20	17, 19	ersym 7375	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
21	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17404	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
22	13, 15, 20, 21	syl3anbrc 1192	. . . . 5 $/\$ $/\$
23	14	ad2antrl 734	. . . . . 6 $/\$ $/\$ $/\$
24	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17404	. . . . . . . 8 $/\$ $/\$ ++ ++ ++ ++
25	24	simp2bi 1024	. . . . . . 7
26	25	ad2antll 735	. . . . . 6 $/\$ $/\$ $/\$
27	16	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$
28	18	ad2antrl 734	. . . . . . 7 $/\$ $/\$ $/\$ ++ ++ ++ ++
29	24	simp3bi 1025	. . . . . . . 8 ++ ++ ++ ++
30	29	ad2antll 735	. . . . . . 7 $/\$ $/\$ $/\$ ++ ++ ++ ++
31	27, 28, 30	ertrd 7379	. . . . . 6 $/\$ $/\$ $/\$ ++ ++ ++ ++
32	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17404	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
33	23, 26, 31, 32	syl3anbrc 1192	. . . . 5 $/\$ $/\$ $/\$
34	16	a1i 11	. . . . . . . . 9 $/\$ $/\$
35		fviss 5923	. . . . . . . . . . . . . 14 Word Word
36	1, 35	eqsstri 3462	. . . . . . . . . . . . 13 Word
37		simpll 760	. . . . . . . . . . . . 13 $/\$ $/\$
38	36, 37	sseldi 3430	. . . . . . . . . . . 12 $/\$ $/\$ Word
39		simpr 463	. . . . . . . . . . . . 13 $/\$ $/\$
40	36, 39	sseldi 3430	. . . . . . . . . . . 12 $/\$ $/\$ Word
41		ccatcl 12720	. . . . . . . . . . . 12 Word $/\$ Word ++ Word
42	38, 40, 41	syl2anc 667	. . . . . . . . . . 11 $/\$ $/\$ ++ Word
43		simplr 762	. . . . . . . . . . . 12 $/\$ $/\$
44	36, 43	sseldi 3430	. . . . . . . . . . 11 $/\$ $/\$ Word
45		ccatcl 12720	. . . . . . . . . . 11 ++ Word $/\$ Word ++ ++ Word
46	42, 44, 45	syl2anc 667	. . . . . . . . . 10 $/\$ $/\$ ++ ++ Word
47	1	efgrcl 17365	. . . . . . . . . . . 12 $/\$ Word
48	47	simprd 465	. . . . . . . . . . 11 Word
49	48	ad2antrr 732	. . . . . . . . . 10 $/\$ $/\$ Word
50	46, 49	eleqtrrd 2532	. . . . . . . . 9 $/\$ $/\$ ++ ++
51	34, 50	erref 7383	. . . . . . . 8 $/\$ $/\$ ++ ++ ++ ++
52	51	ex 436	. . . . . . 7 $/\$ ++ ++ ++ ++
53	52	pm4.71d 640	. . . . . 6 $/\$ $/\$ ++ ++ ++ ++
54	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17404	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++
55		df-3an 987	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++ $/\$ $/\$ ++ ++ ++ ++
56		anidm 650	. . . . . . . 8 $/\$
57	56	anbi1i 701	. . . . . . 7 $/\$ $/\$ ++ ++ ++ ++ $/\$ ++ ++ ++ ++
58	54, 55, 57	3bitri 275	. . . . . 6 $/\$ ++ ++ ++ ++
59	53, 58	syl6bbr 267	. . . . 5 $/\$
60	8, 22, 33, 59	iserd 7389	. . . 4 $/\$
61	1, 2, 3, 4	efgtf 17372	. . . . . . . . . 10 splice $/\$
62	61	simprd 465	. . . . . . . . 9
63	62	adantl 468	. . . . . . . 8 $/\$ $/\$
64		ffn 5728	. . . . . . . 8
65		ovelrn 6445	. . . . . . . 8
66	63, 64, 65	3syl 18	. . . . . . 7 $/\$ $/\$
67		simplr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
68	62	ad2antlr 733	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
69		simprl 764	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
70		simprr 766	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
71	68, 69, 70	fovrnd 6441	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
72	50	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ ++ ++
73	37	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
74	36, 73	sseldi 3430	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Word
75	40	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Word
76		swrdcl 12775	. . . . . . . . . . . . . . . . 17 Word substr Word
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr Word
78		ccatcl 12720	. . . . . . . . . . . . . . . 16 Word $/\$ substr Word ++ substr Word
79	74, 77, 78	syl2anc 667	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr Word
80	3	efgmf 17363	. . . . . . . . . . . . . . . . . 18
81	80	ffvelrni 6021	. . . . . . . . . . . . . . . . 17
82	81	ad2antll 735	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
83	70, 82	s2cld 12965	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Word
84		ccatcl 12720	. . . . . . . . . . . . . . 15 ++ substr Word $/\$ Word ++ substr ++ Word
85	79, 83, 84	syl2anc 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ substr ++ Word
86		swrdcl 12775	. . . . . . . . . . . . . . 15 Word substr Word
87	75, 86	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ substr Word
88	44	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Word
89		ccatass 12732	. . . . . . . . . . . . . 14 ++ substr ++ Word $/\$ substr Word $/\$ Word ++ substr ++ ++ substr ++ ++ substr ++ ++ substr ++
90	85, 87, 88, 89	syl3anc 1268	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ ++ substr ++ ++ substr ++
91		ccatcl 12720	. . . . . . . . . . . . . . . . 17 substr Word $/\$ Word substr ++ Word
92	77, 83, 91	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr ++ Word
93		ccatass 12732	. . . . . . . . . . . . . . . 16 Word $/\$ substr ++ Word $/\$ substr Word ++ substr ++ ++ substr ++ substr ++ ++ substr
94	74, 92, 87, 93	syl3anc 1268	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ substr ++ ++ substr
95		ccatass 12732	. . . . . . . . . . . . . . . . 17 Word $/\$ substr Word $/\$ Word ++ substr ++ ++ substr ++
96	74, 77, 83, 95	syl3anc 1268	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++
97	96	oveq1d 6305	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ substr ++ ++ substr
98	1, 2, 3, 4	efgtval 17373	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ splice
99	67, 69, 70, 98	syl3anc 1268	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ splice
100		splval 12858	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ Word splice substr ++ ++ substr
101	67, 69, 69, 83, 100	syl13anc 1270	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ splice substr ++ ++ substr
102	99, 101	eqtrd 2485	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr ++ ++ substr
103	102	oveq2d 6306	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ ++ substr ++ ++ substr
104	94, 97, 103	3eqtr4rd 2496	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ ++ substr ++ ++ substr
105	104	oveq1d 6305	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ substr ++ ++ substr ++
106		lencl 12687	. . . . . . . . . . . . . . . . . . 19 Word
107	74, 106	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
108		nn0uz 11193	. . . . . . . . . . . . . . . . . 18
109	107, 108	syl6eleq 2539	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
110		elfznn0 11887	. . . . . . . . . . . . . . . . . 18
111	110	ad2antrl 734	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
112		uzaddcl 11215	. . . . . . . . . . . . . . . . 17 $/\$
113	109, 111, 112	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
114	42	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++ Word
115		ccatlen 12721	. . . . . . . . . . . . . . . . . 18 ++ Word $/\$ Word ++ ++ ++
116	114, 88, 115	syl2anc 667	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++ ++ ++
117		ccatlen 12721	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word ++
118	74, 75, 117	syl2anc 667	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ ++
119		elfzuz3 11797	. . . . . . . . . . . . . . . . . . . . . 22
120	119	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
121	107	nn0zd 11038	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
122		eluzadd 11187	. . . . . . . . . . . . . . . . . . . . 21 $/\$
123	120, 121, 122	syl2anc 667	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
124		lencl 12687	. . . . . . . . . . . . . . . . . . . . . . 23 Word
125	75, 124	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
126	125	nn0cnd 10927	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
127	107	nn0cnd 10927	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
128	126, 127	addcomd 9835	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
129	111	nn0cnd 10927	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
130	129, 127	addcomd 9835	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
131	130	fveq2d 5869	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
132	123, 128, 131	3eltr3d 2543	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
133	118, 132	eqeltrd 2529	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++
134		lencl 12687	. . . . . . . . . . . . . . . . . . 19 Word
135	88, 134	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
136		uzaddcl 11215	. . . . . . . . . . . . . . . . . 18 ++ $/\$ ++
137	133, 135, 136	syl2anc 667	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++
138	116, 137	eqeltrd 2529	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ ++
139		elfzuzb 11794	. . . . . . . . . . . . . . . 16 ++ ++ $/\$ ++ ++
140	113, 138, 139	sylanbrc 670	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ ++
141	1, 2, 3, 4	efgtval 17373	. . . . . . . . . . . . . . 15 ++ ++ $/\$ ++ ++ $/\$ ++ ++ ++ ++ splice
142	72, 140, 70, 141	syl3anc 1268	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++ splice
143		wrd0 12691	. . . . . . . . . . . . . . . 16 Word
144	143	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Word
145		ccatcl 12720	. . . . . . . . . . . . . . . 16 substr Word $/\$ Word substr ++ Word
146	87, 88, 145	syl2anc 667	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ substr ++ Word
147		ccatrid 12731	. . . . . . . . . . . . . . . . . 18 ++ substr Word ++ substr ++ ++ substr
148	79, 147	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr
149	148	oveq1d 6305	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ ++ substr ++ ++ substr ++ substr ++
150		ccatass 12732	. . . . . . . . . . . . . . . . 17 ++ substr Word $/\$ substr Word $/\$ Word ++ substr ++ substr ++ ++ substr ++ substr ++
151	79, 87, 88, 150	syl3anc 1268	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++ ++ substr ++ substr ++
152		ccatass 12732	. . . . . . . . . . . . . . . . . . 19 Word $/\$ substr Word $/\$ substr Word ++ substr ++ substr ++ substr ++ substr
153	74, 77, 87, 152	syl3anc 1268	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++ substr ++ substr
154	111, 108	syl6eleq 2539	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
155		eluzfz1 11806	. . . . . . . . . . . . . . . . . . . . . 22
156	154, 155	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
157	125, 108	syl6eleq 2539	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
158		eluzfz2 11807	. . . . . . . . . . . . . . . . . . . . . 22
159	157, 158	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
160		ccatswrd 12812	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ $/\$ substr ++ substr substr
161	75, 156, 69, 159, 160	syl13anc 1270	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
162		swrdid 12784	. . . . . . . . . . . . . . . . . . . . 21 Word substr
163	75, 162	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ substr
164	161, 163	eqtrd 2485	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ substr ++ substr
165	164	oveq2d 6306	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++
166	153, 165	eqtrd 2485	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++
167	166	oveq1d 6305	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr ++ substr ++ ++ ++
168	149, 151, 167	3eqtr2rd 2492	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ substr ++ ++ substr ++
169		ccatlen 12721	. . . . . . . . . . . . . . . . 17 Word $/\$ substr Word ++ substr substr
170	74, 77, 169	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ++ substr substr
171		swrd0len 12778	. . . . . . . . . . . . . . . . . 18 Word $/\$ substr
172	75, 69, 171	syl2anc 667	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ substr
173	172	oveq2d 6306	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ substr
174	170, 173	eqtr2d 2486	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ++ substr
175		hash0 12548	. . . . . . . . . . . . . . . . 17
176	175	oveq2i 6301	. . . . . . . . . . . . . . . 16
177	107, 111	nn0addcld 10929	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
178	177	nn0cnd 10927	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
179	178	addid1d 9833	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
180	176, 179	syl5req 2498	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
181	79, 144, 146, 83, 168, 174, 180	splval2 12864	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ++ ++ splice ++ substr ++ ++ substr ++
182	142, 181	eqtrd 2485	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ substr ++ ++ substr ++
183	90, 105, 182	3eqtr4d 2495	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
184	1, 2, 3, 4	efgtf 17372	. . . . . . . . . . . . . . 15 ++ ++ ++ ++ ++ ++ ++ ++ splice $/\$ ++ ++ ++ ++
185	184	simprd 465	. . . . . . . . . . . . . 14 ++ ++ ++ ++ ++ ++
186		ffn 5728	. . . . . . . . . . . . . 14 ++ ++ ++ ++ ++ ++ ++ ++
187	72, 185, 186	3syl 18	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
188		fnovrn 6444	. . . . . . . . . . . . 13 ++ ++ ++ ++ $/\$ ++ ++ $/\$ ++ ++ ++ ++
189	187, 140, 70, 188	syl3anc 1268	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
190	183, 189	eqeltrd 2529	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
191	1, 2, 3, 4	efgi2 17375	. . . . . . . . . . 11 ++ ++ $/\$ ++ ++ ++ ++ ++ ++ ++ ++
192	72, 190, 191	syl2anc 667	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
193	1, 2, 3, 4, 9, 10, 6	efgcpbllema 17404	. . . . . . . . . 10 $/\$ $/\$ ++ ++ ++ ++
194	67, 71, 192, 193	syl3anbrc 1192	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
195		vex 3048	. . . . . . . . . . 11
196		vex 3048	. . . . . . . . . . 11
197	195, 196	elec 7403	. . . . . . . . . 10
198		breq2 4406	. . . . . . . . . 10
199	197, 198	syl5bb 261	. . . . . . . . 9
200	194, 199	syl5ibrcom 226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
201	200	rexlimdvva 2886	. . . . . . 7 $/\$ $/\$
202	66, 201	sylbid 219	. . . . . 6 $/\$ $/\$
203	202	ssrdv 3438	. . . . 5 $/\$ $/\$
204	203	ralrimiva 2802	. . . 4 $/\$
205		fvex 5875	. . . . . . 7 Word
206	1, 205	eqeltri 2525	. . . . . 6
207		erex 7387	. . . . . 6
208	60, 206, 207	mpisyl 21	. . . . 5 $/\$
209		ereq1 7370	. . . . . . 7
210		eceq2 7401	. . . . . . . . 9
211	210	sseq2d 3460	. . . . . . . 8
212	211	ralbidv 2827	. . . . . . 7
213	209, 212	anbi12d 717	. . . . . 6 $/\$ $/\$
214	213	elabg 3186	. . . . 5 $/\$ $/\$
215	208, 214	syl 17	. . . 4 $/\$ $/\$ $/\$
216	60, 204, 215	mpbir2and 933	. . 3 $/\$ $/\$
217		intss1 4249	. . 3 $/\$ $/\$
218	216, 217	syl 17	. 2 $/\$ $/\$
219	5, 218	syl5eqss 3476	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

cab 2437

wral 2737

wrex 2738

crab 2741

cvv 3045 $\$ cdif 3401

wss 3404

c0 3731

csn 3968

cpr 3970

cop 3974

cotp 3976

cint 4234

ciun 4278 class class class wbr 4402

copab 4460

cmpt 4461

cid 4744

cxp 4832

crn 4835

wrel 4839

wfn 5577

wf 5578

cfv 5582 (class class class)co 6290

cmpt2 6292

c1o 7175

c2o 7176

wer 7360

cec 7361

cc0 9539

c1 9540

caddc 9542

cmin 9860

cn0 10869

cz 10937

cuz 11159

cfz 11784 ..^cfzo 11915

chash 12515 Word cword 12656 ++ cconcat 12658 substr csubstr 12660 splice csplice 12661

cs2 12937 ~_FG cefg 17356

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-ot 3977 df-uni 4199 df-int 4235 df-iun 4280 df-iin 4281 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-ec 7365 df-map 7474 df-pm 7475 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-nn 10610 df-2 10668 df-n0 10870 df-z 10938 df-uz 11160 df-fz 11785 df-fzo 11916 df-hash 12516 df-word 12664 df-concat 12666 df-s1 12667 df-substr 12668 df-splice 12669 df-s2 12944 df-efg 17359

This theorem is referenced by: efgcpbl 17406

W3C validator