Metamath Proof Explorer


Theorem fusgreg2wsplem

Description: Lemma for fusgreg2wsp and related theorems. (Contributed by AV, 8-Jan-2022)

Ref Expression
Hypotheses frgrhash2wsp.v V = Vtx G
fusgreg2wsp.m M = a V w 2 WSPathsN G | w 1 = a
Assertion fusgreg2wsplem N V p M N p 2 WSPathsN G p 1 = N

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v V = Vtx G
2 fusgreg2wsp.m M = a V w 2 WSPathsN G | w 1 = a
3 eqeq2 a = N w 1 = a w 1 = N
4 3 rabbidv a = N w 2 WSPathsN G | w 1 = a = w 2 WSPathsN G | w 1 = N
5 ovex 2 WSPathsN G V
6 5 rabex w 2 WSPathsN G | w 1 = N V
7 4 2 6 fvmpt N V M N = w 2 WSPathsN G | w 1 = N
8 7 eleq2d N V p M N p w 2 WSPathsN G | w 1 = N
9 fveq1 w = p w 1 = p 1
10 9 eqeq1d w = p w 1 = N p 1 = N
11 10 elrab p w 2 WSPathsN G | w 1 = N p 2 WSPathsN G p 1 = N
12 8 11 bitrdi N V p M N p 2 WSPathsN G p 1 = N