Step |
Hyp |
Ref |
Expression |
1 |
|
0pthon.v |
|- V = ( Vtx ` G ) |
2 |
|
0ex |
|- (/) e. _V |
3 |
|
snex |
|- { <. 0 , N >. } e. _V |
4 |
2 3
|
pm3.2i |
|- ( (/) e. _V /\ { <. 0 , N >. } e. _V ) |
5 |
1
|
0pthon1 |
|- ( N e. V -> (/) ( N ( PathsOn ` G ) N ) { <. 0 , N >. } ) |
6 |
|
breq12 |
|- ( ( f = (/) /\ p = { <. 0 , N >. } ) -> ( f ( N ( PathsOn ` G ) N ) p <-> (/) ( N ( PathsOn ` G ) N ) { <. 0 , N >. } ) ) |
7 |
6
|
spc2egv |
|- ( ( (/) e. _V /\ { <. 0 , N >. } e. _V ) -> ( (/) ( N ( PathsOn ` G ) N ) { <. 0 , N >. } -> E. f E. p f ( N ( PathsOn ` G ) N ) p ) ) |
8 |
4 5 7
|
mpsyl |
|- ( N e. V -> E. f E. p f ( N ( PathsOn ` G ) N ) p ) |