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 e. V |-> { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = a } )
Assertion fusgreg2wsplem 
|- ( N e. V -> ( p e. ( M ` N ) <-> ( p e. ( 2 WSPathsN G ) /\ ( p ` 1 ) = N ) ) )

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v 
 |-  V = ( Vtx ` G )
2 fusgreg2wsp.m 
 |-  M = ( a e. V |-> { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = a } )
3 eqeq2 
 |-  ( a = N -> ( ( w ` 1 ) = a <-> ( w ` 1 ) = N ) )
4 3 rabbidv 
 |-  ( a = N -> { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = a } = { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = N } )
5 ovex 
 |-  ( 2 WSPathsN G ) e. _V
6 5 rabex 
 |-  { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = N } e. _V
7 4 2 6 fvmpt 
 |-  ( N e. V -> ( M ` N ) = { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = N } )
8 7 eleq2d 
 |-  ( N e. V -> ( p e. ( M ` N ) <-> p e. { w e. ( 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 e. { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = N } <-> ( p e. ( 2 WSPathsN G ) /\ ( p ` 1 ) = N ) )
12 8 11 bitrdi 
 |-  ( N e. V -> ( p e. ( M ` N ) <-> ( p e. ( 2 WSPathsN G ) /\ ( p ` 1 ) = N ) ) )