Metamath Proof Explorer

Theorem wspthsn

Description: The set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 11-May-2021)

Ref Expression
Assertion wspthsn 
|- ( N WSPathsN G ) = { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w }

Proof

Step Hyp Ref Expression
1 oveq12 
 |-  ( ( n = N /\ g = G ) -> ( n WWalksN g ) = ( N WWalksN G ) )
2 fveq2 
 |-  ( g = G -> ( SPaths ` g ) = ( SPaths ` G ) )
3 2 breqd 
 |-  ( g = G -> ( f ( SPaths ` g ) w <-> f ( SPaths ` G ) w ) )
4 3 exbidv 
 |-  ( g = G -> ( E. f f ( SPaths ` g ) w <-> E. f f ( SPaths ` G ) w ) )
5 4 adantl 
 |-  ( ( n = N /\ g = G ) -> ( E. f f ( SPaths ` g ) w <-> E. f f ( SPaths ` G ) w ) )
6 1 5 rabeqbidv 
 |-  ( ( n = N /\ g = G ) -> { w e. ( n WWalksN g ) | E. f f ( SPaths ` g ) w } = { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w } )
7 df-wspthsn 
 |-  WSPathsN = ( n e. NN0 , g e. _V |-> { w e. ( n WWalksN g ) | E. f f ( SPaths ` g ) w } )
8 ovex 
 |-  ( N WWalksN G ) e. _V
9 8 rabex 
 |-  { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w } e. _V
10 6 7 9 ovmpoa 
 |-  ( ( N e. NN0 /\ G e. _V ) -> ( N WSPathsN G ) = { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w } )
11 7 mpondm0 
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> ( N WSPathsN G ) = (/) )
12 df-wwlksn 
 |-  WWalksN = ( n e. NN0 , g e. _V |-> { w e. ( WWalks ` g ) | ( # ` w ) = ( n + 1 ) } )
13 12 mpondm0 
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> ( N WWalksN G ) = (/) )
14 13 rabeqdv 
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w } = { w e. (/) | E. f f ( SPaths ` G ) w } )
15 rab0 
 |-  { w e. (/) | E. f f ( SPaths ` G ) w } = (/)
16 14 15 eqtrdi 
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w } = (/) )
17 11 16 eqtr4d 
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> ( N WSPathsN G ) = { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w } )
18 10 17 pm2.61i 
 |-  ( N WSPathsN G ) = { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w }