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

Theorem efgred2 15078
 Description: Two extension sequences have related endpoints iff they have the same base. (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 ..^
Assertion
Ref Expression
efgred2
Distinct variable groups:   ,   ,,,,,,,   ,   ,,,,,   ,,,,   ,,,,,,,,,   ,,,,,   ,,,,,,,,   ,,
Allowed substitution hints:   (,,,,,,,,)   (,,,,,,,,)   (,,,,,,)   (,,,)   (,,,,,,,,)   (,,,,)   ()   (,,)

Proof of Theorem efgred2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . . . . . . 8 Word
2 efgval.r . . . . . . . 8 ~FG
3 efgval2.m . . . . . . . 8
4 efgval2.t . . . . . . . 8 splice
5 efgred.d . . . . . . . 8
6 efgred.s . . . . . . . 8 Word ..^
71, 2, 3, 4, 5, 6efgsfo 15064 . . . . . . 7
8 fof 5467 . . . . . . 7
97, 8ax-mp 8 . . . . . 6
109ffvelrni 5680 . . . . 5
1110ad2antlr 707 . . . 4
121, 2, 3, 4, 5, 6efgredeu 15077 . . . 4
13 reu5 2766 . . . . 5
1413simprbi 450 . . . 4
1511, 12, 143syl 18 . . 3
161, 2, 3, 4, 5, 6efgsdm 15055 . . . . 5 Word ..^
1716simp2bi 971 . . . 4
191, 2efger 15043 . . . . 5
2019a1i 10 . . . 4
211, 2, 3, 4, 5, 6efgsrel 15059 . . . . 5
2221ad2antrr 706 . . . 4
23 simpr 447 . . . 4
2420, 22, 23ertrd 6692 . . 3
251, 2, 3, 4, 5, 6efgsdm 15055 . . . . 5 Word ..^
2625simp2bi 971 . . . 4
281, 2, 3, 4, 5, 6efgsrel 15059 . . . 4