Step |
Hyp |
Ref |
Expression |
1 |
|
0pthon.v |
|- V = ( Vtx ` G ) |
2 |
1
|
0trlon |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( N ( TrailsOn ` G ) N ) P ) |
3 |
|
simpl |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> P : ( 0 ... 0 ) --> V ) |
4 |
|
id |
|- ( P : ( 0 ... 0 ) --> V -> P : ( 0 ... 0 ) --> V ) |
5 |
|
0z |
|- 0 e. ZZ |
6 |
|
elfz3 |
|- ( 0 e. ZZ -> 0 e. ( 0 ... 0 ) ) |
7 |
5 6
|
mp1i |
|- ( P : ( 0 ... 0 ) --> V -> 0 e. ( 0 ... 0 ) ) |
8 |
4 7
|
ffvelrnd |
|- ( P : ( 0 ... 0 ) --> V -> ( P ` 0 ) e. V ) |
9 |
8
|
adantr |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( P ` 0 ) e. V ) |
10 |
|
eleq1 |
|- ( ( P ` 0 ) = N -> ( ( P ` 0 ) e. V <-> N e. V ) ) |
11 |
10
|
adantl |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( ( P ` 0 ) e. V <-> N e. V ) ) |
12 |
9 11
|
mpbid |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> N e. V ) |
13 |
1
|
1vgrex |
|- ( N e. V -> G e. _V ) |
14 |
1
|
0pth |
|- ( G e. _V -> ( (/) ( Paths ` G ) P <-> P : ( 0 ... 0 ) --> V ) ) |
15 |
12 13 14
|
3syl |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( (/) ( Paths ` G ) P <-> P : ( 0 ... 0 ) --> V ) ) |
16 |
3 15
|
mpbird |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( Paths ` G ) P ) |
17 |
1
|
0wlkonlem1 |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( N e. V /\ N e. V ) ) |
18 |
1
|
0wlkonlem2 |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> P e. ( V ^pm ( 0 ... 0 ) ) ) |
19 |
|
0ex |
|- (/) e. _V |
20 |
18 19
|
jctil |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( (/) e. _V /\ P e. ( V ^pm ( 0 ... 0 ) ) ) ) |
21 |
1
|
ispthson |
|- ( ( ( N e. V /\ N e. V ) /\ ( (/) e. _V /\ P e. ( V ^pm ( 0 ... 0 ) ) ) ) -> ( (/) ( N ( PathsOn ` G ) N ) P <-> ( (/) ( N ( TrailsOn ` G ) N ) P /\ (/) ( Paths ` G ) P ) ) ) |
22 |
17 20 21
|
syl2anc |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( (/) ( N ( PathsOn ` G ) N ) P <-> ( (/) ( N ( TrailsOn ` G ) N ) P /\ (/) ( Paths ` G ) P ) ) ) |
23 |
2 16 22
|
mpbir2and |
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( N ( PathsOn ` G ) N ) P ) |