Step |
Hyp |
Ref |
Expression |
1 |
|
usgr2trlncl |
|- ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Trails ` G ) P -> ( P ` 0 ) =/= ( P ` 2 ) ) ) |
2 |
1
|
imp |
|- ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ F ( Trails ` G ) P ) -> ( P ` 0 ) =/= ( P ` 2 ) ) |
3 |
|
trliswlk |
|- ( F ( Trails ` G ) P -> F ( Walks ` G ) P ) |
4 |
|
wlkonwlk |
|- ( F ( Walks ` G ) P -> F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P ) |
5 |
|
simpll |
|- ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> G e. USGraph ) |
6 |
|
simplr |
|- ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> ( # ` F ) = 2 ) |
7 |
|
fveq2 |
|- ( ( # ` F ) = 2 -> ( P ` ( # ` F ) ) = ( P ` 2 ) ) |
8 |
7
|
eqcomd |
|- ( ( # ` F ) = 2 -> ( P ` 2 ) = ( P ` ( # ` F ) ) ) |
9 |
8
|
neeq2d |
|- ( ( # ` F ) = 2 -> ( ( P ` 0 ) =/= ( P ` 2 ) <-> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) |
10 |
9
|
biimpd |
|- ( ( # ` F ) = 2 -> ( ( P ` 0 ) =/= ( P ` 2 ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) |
11 |
10
|
adantl |
|- ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( P ` 0 ) =/= ( P ` 2 ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) |
12 |
11
|
imp |
|- ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) |
13 |
|
usgr2wlkspth |
|- ( ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P <-> F ( ( P ` 0 ) ( SPathsOn ` G ) ( P ` ( # ` F ) ) ) P ) ) |
14 |
5 6 12 13
|
syl3anc |
|- ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P <-> F ( ( P ` 0 ) ( SPathsOn ` G ) ( P ` ( # ` F ) ) ) P ) ) |
15 |
|
spthonisspth |
|- ( F ( ( P ` 0 ) ( SPathsOn ` G ) ( P ` ( # ` F ) ) ) P -> F ( SPaths ` G ) P ) |
16 |
14 15
|
syl6bi |
|- ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P -> F ( SPaths ` G ) P ) ) |
17 |
16
|
expcom |
|- ( ( P ` 0 ) =/= ( P ` 2 ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P -> F ( SPaths ` G ) P ) ) ) |
18 |
17
|
com13 |
|- ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( P ` 0 ) =/= ( P ` 2 ) -> F ( SPaths ` G ) P ) ) ) |
19 |
3 4 18
|
3syl |
|- ( F ( Trails ` G ) P -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( P ` 0 ) =/= ( P ` 2 ) -> F ( SPaths ` G ) P ) ) ) |
20 |
19
|
impcom |
|- ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ F ( Trails ` G ) P ) -> ( ( P ` 0 ) =/= ( P ` 2 ) -> F ( SPaths ` G ) P ) ) |
21 |
2 20
|
mpd |
|- ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ F ( Trails ` G ) P ) -> F ( SPaths ` G ) P ) |
22 |
21
|
ex |
|- ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Trails ` G ) P -> F ( SPaths ` G ) P ) ) |
23 |
|
spthispth |
|- ( F ( SPaths ` G ) P -> F ( Paths ` G ) P ) |
24 |
|
pthistrl |
|- ( F ( Paths ` G ) P -> F ( Trails ` G ) P ) |
25 |
23 24
|
syl |
|- ( F ( SPaths ` G ) P -> F ( Trails ` G ) P ) |
26 |
22 25
|
impbid1 |
|- ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Trails ` G ) P <-> F ( SPaths ` G ) P ) ) |