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.
StepHypRef Expression
1 efgval.w . . 3 Word
2 efgval.r . . 3 ~FG
3 efgval2.m . . 3
4 efgval2.t . . 3 splice
51, 2, 3, 4efgval2 17452 . 2
6 efgcpbllem.1 . . . . . . 7 ++ ++ ++ ++
76relopabi 4964 . . . . . 6
87a1i 11 . . . . 5
9 efgred.d . . . . . . . . 9
10 efgred.s . . . . . . . . 9 Word ..^
111, 2, 3, 4, 9, 10, 6efgcpbllema 17482 . . . . . . . 8 ++ ++ ++ ++
1211simp2bi 1046 . . . . . . 7
1312adantl 473 . . . . . 6
1411simp1bi 1045 . . . . . . 7
1514adantl 473 . . . . . 6
161, 2efger 17446 . . . . . . . 8
1716a1i 11 . . . . . . 7
1811simp3bi 1047 . . . . . . . 8 ++ ++ ++ ++
1918adantl 473 . . . . . . 7 ++ ++ ++ ++
2017, 19ersym 7393 . . . . . 6 ++ ++ ++ ++
211, 2, 3, 4, 9, 10, 6efgcpbllema 17482 . . . . . 6 ++ ++ ++ ++
2213, 15, 20, 21syl3anbrc 1214 . . . . 5
2314ad2antrl 742 . . . . . 6
241, 2, 3, 4, 9, 10, 6efgcpbllema 17482 . . . . . . . 8 ++ ++ ++ ++
2524simp2bi 1046 . . . . . . 7
2625ad2antll 743 . . . . . 6
2716a1i 11 . . . . . . 7
2818ad2antrl 742 . . . . . . 7 ++ ++ ++ ++
2924simp3bi 1047 . . . . . . . 8 ++ ++ ++ ++
3029ad2antll 743 . . . . . . 7 ++ ++ ++ ++
3127, 28, 30ertrd 7397 . . . . . 6 ++ ++ ++ ++
321, 2, 3, 4, 9, 10, 6efgcpbllema 17482 . . . . . 6 ++ ++ ++ ++
3323, 26, 31, 32syl3anbrc 1214 . . . . 5
3416a1i 11 . . . . . . . . 9
35 fviss 5938 . . . . . . . . . . . . . 14 Word Word
361, 35eqsstri 3448 . . . . . . . . . . . . 13 Word
37 simpll 768 . . . . . . . . . . . . 13
3836, 37sseldi 3416 . . . . . . . . . . . 12 Word
39 simpr 468 . . . . . . . . . . . . 13
4036, 39sseldi 3416 . . . . . . . . . . . 12 Word
41 ccatcl 12771 . . . . . . . . . . . 12 Word Word ++ Word
4238, 40, 41syl2anc 673 . . . . . . . . . . 11 ++ Word
43 simplr 770 . . . . . . . . . . . 12
4436, 43sseldi 3416 . . . . . . . . . . 11 Word
45 ccatcl 12771 . . . . . . . . . . 11 ++ Word Word ++ ++ Word
4642, 44, 45syl2anc 673 . . . . . . . . . 10 ++ ++ Word
471efgrcl 17443 . . . . . . . . . . . 12 Word
4847simprd 470 . . . . . . . . . . 11 Word
4948ad2antrr 740 . . . . . . . . . 10 Word
5046, 49eleqtrrd 2552 . . . . . . . . 9 ++ ++
5134, 50erref 7401 . . . . . . . 8 ++ ++ ++ ++
5251ex 441 . . . . . . 7 ++ ++ ++ ++
5352pm4.71d 646 . . . . . 6 ++ ++ ++ ++
541, 2, 3, 4, 9, 10, 6efgcpbllema 17482 . . . . . . 7 ++ ++ ++ ++
55 df-3an 1009 . . . . . . 7 ++ ++ ++ ++ ++ ++ ++ ++
56 anidm 656 . . . . . . . 8
5756anbi1i 709 . . . . . . 7 ++ ++ ++ ++ ++ ++ ++ ++
5854, 55, 573bitri 279 . . . . . 6 ++ ++ ++ ++
5953, 58syl6bbr 271 . . . . 5
608, 22, 33, 59iserd 7407 . . . 4
611, 2, 3, 4efgtf 17450 . . . . . . . . . 10 splice
6261simprd 470 . . . . . . . . 9
6362adantl 473 . . . . . . . 8
64 ffn 5739 . . . . . . . 8
65 ovelrn 6464 . . . . . . . 8
6663, 64, 653syl 18 . . . . . . 7
67 simplr 770 . . . . . . . . . 10
6862ad2antlr 741 . . . . . . . . . . 11
69 simprl 772 . . . . . . . . . . 11
70 simprr 774 . . . . . . . . . . 11
7168, 69, 70fovrnd 6460 . . . . . . . . . 10
7250adantr 472 . . . . . . . . . . 11 ++ ++
7337adantr 472 . . . . . . . . . . . . . . . . 17
7436, 73sseldi 3416 . . . . . . . . . . . . . . . 16 Word
7540adantr 472 . . . . . . . . . . . . . . . . 17 Word
76 swrdcl 12829 . . . . . . . . . . . . . . . . 17 Word substr Word
7775, 76syl 17 . . . . . . . . . . . . . . . 16 substr Word
78 ccatcl 12771 . . . . . . . . . . . . . . . 16 Word substr Word ++ substr Word
7974, 77, 78syl2anc 673 . . . . . . . . . . . . . . 15 ++ substr Word
803efgmf 17441 . . . . . . . . . . . . . . . . . 18
8180ffvelrni 6036 . . . . . . . . . . . . . . . . 17
8281ad2antll 743 . . . . . . . . . . . . . . . 16
8370, 82s2cld 13025 . . . . . . . . . . . . . . 15 Word
84 ccatcl 12771 . . . . . . . . . . . . . . 15 ++ substr Word Word ++ substr ++ Word
8579, 83, 84syl2anc 673 . . . . . . . . . . . . . 14 ++ substr ++ Word
86 swrdcl 12829 . . . . . . . . . . . . . . 15 Word substr Word
8775, 86syl 17 . . . . . . . . . . . . . 14 substr Word
8844adantr 472 . . . . . . . . . . . . . 14 Word
89 ccatass 12783 . . . . . . . . . . . . . 14 ++ substr ++ Word substr Word Word ++ substr ++ ++ substr ++ ++ substr ++ ++ substr ++
9085, 87, 88, 89syl3anc 1292 . . . . . . . . . . . . 13 ++ substr ++ ++ substr ++ ++ substr ++ ++ substr ++
91 ccatcl 12771 . . . . . . . . . . . . . . . . 17 substr Word Word substr ++ Word
9277, 83, 91syl2anc 673 . . . . . . . . . . . . . . . 16 substr ++ Word
93 ccatass 12783 . . . . . . . . . . . . . . . 16 Word substr ++ Word substr Word ++ substr ++ ++ substr ++ substr ++ ++ substr
9474, 92, 87, 93syl3anc 1292 . . . . . . . . . . . . . . 15 ++ substr ++ ++ substr ++ substr ++ ++ substr
95 ccatass 12783 . . . . . . . . . . . . . . . . 17 Word substr Word Word ++ substr ++ ++ substr ++
9674, 77, 83, 95syl3anc 1292 . . . . . . . . . . . . . . . 16 ++ substr ++ ++ substr ++
9796oveq1d 6323 . . . . . . . . . . . . . . 15 ++ substr ++ ++ substr ++ substr ++ ++ substr
981, 2, 3, 4efgtval 17451 . . . . . . . . . . . . . . . . . 18 splice
9967, 69, 70, 98syl3anc 1292 . . . . . . . . . . . . . . . . 17 splice
100 splval 12912 . . . . . . . . . . . . . . . . . 18 Word splice substr ++ ++ substr
10167, 69, 69, 83, 100syl13anc 1294 . . . . . . . . . . . . . . . . 17 splice substr ++ ++ substr
10299, 101eqtrd 2505 . . . . . . . . . . . . . . . 16 substr ++ ++ substr
103102oveq2d 6324 . . . . . . . . . . . . . . 15 ++ ++ substr ++ ++ substr
10494, 97, 1033eqtr4rd 2516 . . . . . . . . . . . . . 14 ++ ++ substr ++ ++ substr
105104oveq1d 6323 . . . . . . . . . . . . 13 ++ ++ ++ substr ++ ++ substr ++
106 lencl 12737 . . . . . . . . . . . . . . . . . . 19 Word
10774, 106syl 17 . . . . . . . . . . . . . . . . . 18
108 nn0uz 11217 . . . . . . . . . . . . . . . . . 18
109107, 108syl6eleq 2559 . . . . . . . . . . . . . . . . 17
110 elfznn0 11913 . . . . . . . . . . . . . . . . . 18
111110ad2antrl 742 . . . . . . . . . . . . . . . . 17
112 uzaddcl 11238 . . . . . . . . . . . . . . . . 17
113109, 111, 112syl2anc 673 . . . . . . . . . . . . . . . 16
11442adantr 472 . . . . . . . . . . . . . . . . . 18 ++ Word
115 ccatlen 12772 . . . . . . . . . . . . . . . . . 18 ++ Word Word ++ ++ ++
116114, 88, 115syl2anc 673 . . . . . . . . . . . . . . . . 17 ++ ++ ++
117 ccatlen 12772 . . . . . . . . . . . . . . . . . . . 20 Word Word ++
11874, 75, 117syl2anc 673 . . . . . . . . . . . . . . . . . . 19 ++
119 elfzuz3 11823 . . . . . . . . . . . . . . . . . . . . . 22
120119ad2antrl 742 . . . . . . . . . . . . . . . . . . . . 21
121107nn0zd 11061 . . . . . . . . . . . . . . . . . . . . 21
122 eluzadd 11211 . . . . . . . . . . . . . . . . . . . . 21
123120, 121, 122syl2anc 673 . . . . . . . . . . . . . . . . . . . 20
124 lencl 12737 . . . . . . . . . . . . . . . . . . . . . . 23 Word
12575, 124syl 17 . . . . . . . . . . . . . . . . . . . . . 22
126125nn0cnd 10951 . . . . . . . . . . . . . . . . . . . . 21
127107nn0cnd 10951 . . . . . . . . . . . . . . . . . . . . 21
128126, 127addcomd 9853 . . . . . . . . . . . . . . . . . . . 20
129111nn0cnd 10951 . . . . . . . . . . . . . . . . . . . . . 22
130129, 127addcomd 9853 . . . . . . . . . . . . . . . . . . . . 21
131130fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20
132123, 128, 1313eltr3d 2563 . . . . . . . . . . . . . . . . . . 19
133118, 132eqeltrd 2549 . . . . . . . . . . . . . . . . . 18 ++
134 lencl 12737 . . . . . . . . . . . . . . . . . . 19 Word
13588, 134syl 17 . . . . . . . . . . . . . . . . . 18
136 uzaddcl 11238 . . . . . . . . . . . . . . . . . 18 ++ ++
137133, 135, 136syl2anc 673 . . . . . . . . . . . . . . . . 17 ++
138116, 137eqeltrd 2549 . . . . . . . . . . . . . . . 16 ++ ++
139 elfzuzb 11820 . . . . . . . . . . . . . . . 16 ++ ++ ++ ++
140113, 138, 139sylanbrc 677 . . . . . . . . . . . . . . 15 ++ ++
1411, 2, 3, 4efgtval 17451 . . . . . . . . . . . . . . 15 ++ ++ ++ ++ ++ ++ ++ ++ splice
14272, 140, 70, 141syl3anc 1292 . . . . . . . . . . . . . 14 ++ ++ ++ ++ splice
143 wrd0 12742 . . . . . . . . . . . . . . . 16 Word
144143a1i 11 . . . . . . . . . . . . . . 15 Word
145 ccatcl 12771 . . . . . . . . . . . . . . . 16 substr Word Word substr ++ Word
14687, 88, 145syl2anc 673 . . . . . . . . . . . . . . 15 substr ++ Word
147 ccatrid 12782 . . . . . . . . . . . . . . . . . 18 ++ substr Word ++ substr ++ ++ substr
14879, 147syl 17 . . . . . . . . . . . . . . . . 17 ++ substr ++ ++ substr
149148oveq1d 6323 . . . . . . . . . . . . . . . 16 ++ substr ++ ++ substr ++ ++ substr ++ substr ++
150 ccatass 12783 . . . . . . . . . . . . . . . . 17 ++ substr Word substr Word Word ++ substr ++ substr ++ ++ substr ++ substr ++
15179, 87, 88, 150syl3anc 1292 . . . . . . . . . . . . . . . 16 ++ substr ++ substr ++ ++ substr ++ substr ++
152 ccatass 12783 . . . . . . . . . . . . . . . . . . 19 Word substr Word substr Word ++ substr ++ substr ++ substr ++ substr
15374, 77, 87, 152syl3anc 1292 . . . . . . . . . . . . . . . . . 18 ++ substr ++ substr ++ substr ++ substr
154111, 108syl6eleq 2559 . . . . . . . . . . . . . . . . . . . . . 22
155 eluzfz1 11832 . . . . . . . . . . . . . . . . . . . . . 22
156154, 155syl 17 . . . . . . . . . . . . . . . . . . . . 21
157125, 108syl6eleq 2559 . . . . . . . . . . . . . . . . . . . . . 22
158 eluzfz2 11833 . . . . . . . . . . . . . . . . . . . . . 22
159157, 158syl 17 . . . . . . . . . . . . . . . . . . . . 21
160 ccatswrd 12866 . . . . . . . . . . . . . . . . . . . . 21 Word substr ++ substr substr
16175, 156, 69, 159, 160syl13anc 1294 . . . . . . . . . . . . . . . . . . . 20 substr ++ substr substr
162 swrdid 12838 . . . . . . . . . . . . . . . . . . . . 21 Word substr
16375, 162syl 17 . . . . . . . . . . . . . . . . . . . 20 substr
164161, 163eqtrd 2505 . . . . . . . . . . . . . . . . . . 19 substr ++ substr
165164oveq2d 6324 . . . . . . . . . . . . . . . . . 18 ++ substr ++ substr ++
166153, 165eqtrd 2505 . . . . . . . . . . . . . . . . 17 ++ substr ++ substr ++
167166oveq1d 6323 . . . . . . . . . . . . . . . 16 ++ substr ++ substr ++ ++ ++
168149, 151, 1673eqtr2rd 2512 . . . . . . . . . . . . . . 15 ++ ++ ++ substr ++ ++ substr ++
169 ccatlen 12772 . . . . . . . . . . . . . . . . 17 Word substr Word ++ substr substr
17074, 77, 169syl2anc 673 . . . . . . . . . . . . . . . 16 ++ substr substr
171 swrd0len 12832 . . . . . . . . . . . . . . . . . 18 Word substr
17275, 69, 171syl2anc 673 . . . . . . . . . . . . . . . . 17 substr
173172oveq2d 6324 . . . . . . . . . . . . . . . 16 substr
174170, 173eqtr2d 2506 . . . . . . . . . . . . . . 15 ++ substr
175 hash0 12586 . . . . . . . . . . . . . . . . 17
176175oveq2i 6319 . . . . . . . . . . . . . . . 16
177107, 111nn0addcld 10953 . . . . . . . . . . . . . . . . . 18
178177nn0cnd 10951 . . . . . . . . . . . . . . . . 17
179178addid1d 9851 . . . . . . . . . . . . . . . 16
180176, 179syl5req 2518 . . . . . . . . . . . . . . 15
18179, 144, 146, 83, 168, 174, 180splval2 12918 . . . . . . . . . . . . . 14 ++ ++ splice ++ substr ++ ++ substr ++
182142, 181eqtrd 2505 . . . . . . . . . . . . 13 ++ ++ ++ substr ++ ++ substr ++
18390, 105, 1823eqtr4d 2515 . . . . . . . . . . . 12 ++ ++ ++ ++
1841, 2, 3, 4efgtf 17450 . . . . . . . . . . . . . . 15 ++ ++ ++ ++ ++ ++ ++ ++ splice ++ ++ ++ ++
185184simprd 470 . . . . . . . . . . . . . 14 ++ ++ ++ ++ ++ ++
186 ffn 5739 . . . . . . . . . . . . . 14 ++ ++ ++ ++ ++ ++ ++ ++
18772, 185, 1863syl 18 . . . . . . . . . . . . 13 ++ ++ ++ ++
188 fnovrn 6463 . . . . . . . . . . . . 13 ++ ++ ++ ++ ++ ++ ++ ++ ++ ++
189187, 140, 70, 188syl3anc 1292 . . . . . . . . . . . 12 ++ ++ ++ ++
190183, 189eqeltrd 2549 . . . . . . . . . . 11 ++ ++ ++ ++
1911, 2, 3, 4efgi2 17453 . . . . . . . . . . 11 ++ ++ ++ ++ ++ ++ ++ ++ ++ ++
19272, 190, 191syl2anc 673 . . . . . . . . . 10 ++ ++ ++ ++
1931, 2, 3, 4, 9, 10, 6efgcpbllema 17482 . . . . . . . . . 10 ++ ++ ++ ++
19467, 71, 192, 193syl3anbrc 1214 . . . . . . . . 9
195 vex 3034 . . . . . . . . . . 11
196 vex 3034 . . . . . . . . . . 11
197195, 196elec 7421 . . . . . . . . . 10
198 breq2 4399 . . . . . . . . . 10
199197, 198syl5bb 265 . . . . . . . . 9
200194, 199syl5ibrcom 230 . . . . . . . 8
201200rexlimdvva 2878 . . . . . . 7
20266, 201sylbid 223 . . . . . 6
203202ssrdv 3424 . . . . 5
204203ralrimiva 2809 . . . 4
205 fvex 5889 . . . . . . 7 Word
2061, 205eqeltri 2545 . . . . . 6
207 erex 7405 . . . . . 6
20860, 206, 207mpisyl 21 . . . . 5
209 ereq1 7388 . . . . . . 7
210 eceq2 7419 . . . . . . . . 9
211210sseq2d 3446 . . . . . . . 8
212211ralbidv 2829 . . . . . . 7
213209, 212anbi12d 725 . . . . . 6
214213elabg 3174 . . . . 5
215208, 214syl 17 . . . 4
21660, 204, 215mpbir2and 936 . . 3
217 intss1 4241 . . 3
218216, 217syl 17 . 2
2195, 218syl5eqss 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
 Copyright terms: Public domain W3C validator