Metamath Proof Explorer

Theorem wspthnp

Description: Properties of a set being a simple path of a fixed length as word. (Contributed by AV, 18-May-2021)

Ref Expression
Assertion wspthnp 
|- ( W e. ( N WSPathsN G ) -> ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) )

Proof

Step Hyp Ref Expression
1 df-wspthsn 
 |-  WSPathsN = ( n e. NN0 , g e. _V |-> { w e. ( n WWalksN g ) | E. f f ( SPaths ` g ) w } )
2 1 elmpocl 
 |-  ( W e. ( N WSPathsN G ) -> ( N e. NN0 /\ G e. _V ) )
3 simpl 
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WSPathsN G ) ) -> ( N e. NN0 /\ G e. _V ) )
4 iswspthn 
 |-  ( W e. ( N WSPathsN G ) <-> ( W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) )
5 4 bilani 
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WSPathsN G ) ) -> ( W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) )
6 3anass 
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) <-> ( ( N e. NN0 /\ G e. _V ) /\ ( W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) ) )
7 3 5 6 sylanbrc 
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WSPathsN G ) ) -> ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) )
8 2 7 mpancom 
 |-  ( W e. ( N WSPathsN G ) -> ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) )