Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
2 |
1
|
wspthnonp |
|- ( w e. ( A ( N WSPathsNOn G ) B ) -> ( ( N e. NN0 /\ G e. _V ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( w e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) ) ) |
3 |
|
simp3l |
|- ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( w e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) ) -> w e. ( A ( N WWalksNOn G ) B ) ) |
4 |
2 3
|
syl |
|- ( w e. ( A ( N WSPathsNOn G ) B ) -> w e. ( A ( N WWalksNOn G ) B ) ) |
5 |
4
|
ssriv |
|- ( A ( N WSPathsNOn G ) B ) C_ ( A ( N WWalksNOn G ) B ) |