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

Theorem efgrelexlema 16638
 Description: If two words are related under the free group equivalence, then there exist two extension sequences such that ends at , ends at , and and have the same starting point. (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 ..^
efgrelexlem.1
Assertion
Ref Expression
efgrelexlema
Distinct variable groups:   ,,,,,,   ,,,   ,,   ,,,,,,   ,,,,,,,,,,,   ,,,,,,,,,   ,,,   ,,,,,,,,,,,,   ,,,,,,,,,,,   ,,,,,,   ,,,,,,   ,,,,,,,,,,,,,   ,,,,,,,,
Allowed substitution hints:   (,,,,,,,,)   (,,,,,,,,)   (,,,,,,)   (,,,)   (,,,,,,,,)   (,,,,,)   (,)   (,,,,,,,,,,,,)   (,,,)

Proof of Theorem efgrelexlema
StepHypRef Expression
1 efgrelexlem.1 . . 3
21bropaex12 5060 . 2
3 n0i 3773 . . . . . 6
4 snprc 4075 . . . . . . . 8
5 imaeq2 5320 . . . . . . . 8
64, 5sylbi 195 . . . . . . 7
7 ima0 5339 . . . . . . 7
86, 7syl6eq 2498 . . . . . 6
93, 8nsyl2 127 . . . . 5
10 n0i 3773 . . . . . 6
11 snprc 4075 . . . . . . . 8
12 imaeq2 5320 . . . . . . . 8
1311, 12sylbi 195 . . . . . . 7
1413, 7syl6eq 2498 . . . . . 6
1510, 14nsyl2 127 . . . . 5
169, 15anim12i 566 . . . 4
1716a1d 25 . . 3
1817rexlimivv 2938 . 2
19 fveq1 5852 . . . . . 6
2019eqeq1d 2443 . . . . 5
21 fveq1 5852 . . . . . 6
2221eqeq2d 2455 . . . . 5
2320, 22cbvrex2v 3077 . . . 4
24 sneq 4021 . . . . . 6
2524imaeq2d 5324 . . . . 5
2625rexeqdv 3045 . . . 4
2723, 26syl5bb 257 . . 3
28 sneq 4021 . . . . . 6
2928imaeq2d 5324 . . . . 5
3029rexeqdv 3045 . . . 4
3130rexbidv 2952 . . 3
3227, 31, 1brabg 4753 . 2
332, 18, 32pm5.21nii 353 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wb 184   wa 369   wceq 1381   wcel 1802  wral 2791  wrex 2792  crab 2795  cvv 3093   cdif 3456  c0 3768  csn 4011  cop 4017  cotp 4019  ciun 4312   class class class wbr 4434  copab 4491   cmpt 4492   cid 4777   cxp 4984  ccnv 4985   crn 4987  cima 4989  cfv 5575  (class class class)co 6278   cmpt2 6280  c1o 7122  c2o 7123  cc0 9492  c1 9493   cmin 9807  cfz 11678  ..^cfzo 11800  chash 12381  Word cword 12510   splice csplice 12515  cs2 12782   ~FG cefg 16595 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pr 4673 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-br 4435  df-opab 4493  df-xp 4992  df-cnv 4994  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fv 5583 This theorem is referenced by:  efgrelexlemb  16639  efgrelex  16640
 Copyright terms: Public domain W3C validator