Step |
Hyp |
Ref |
Expression |
1 |
|
simpl31 |
|- ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> F ( Walks ` G ) P ) |
2 |
|
uhgrwkspthlem1 |
|- ( ( F ( Walks ` G ) P /\ ( # ` F ) = 1 ) -> Fun `' F ) |
3 |
2
|
expcom |
|- ( ( # ` F ) = 1 -> ( F ( Walks ` G ) P -> Fun `' F ) ) |
4 |
3
|
3ad2ant2 |
|- ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( F ( Walks ` G ) P -> Fun `' F ) ) |
5 |
4
|
com12 |
|- ( F ( Walks ` G ) P -> ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> Fun `' F ) ) |
6 |
5
|
3ad2ant1 |
|- ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> Fun `' F ) ) |
7 |
6
|
3ad2ant3 |
|- ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> Fun `' F ) ) |
8 |
7
|
imp |
|- ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> Fun `' F ) |
9 |
|
istrl |
|- ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) ) |
10 |
1 8 9
|
sylanbrc |
|- ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> F ( Trails ` G ) P ) |
11 |
|
3simpc |
|- ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( ( # ` F ) = 1 /\ A =/= B ) ) |
12 |
11
|
adantl |
|- ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( ( # ` F ) = 1 /\ A =/= B ) ) |
13 |
|
3simpc |
|- ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) |
14 |
13
|
3ad2ant3 |
|- ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) |
15 |
14
|
adantr |
|- ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) |
16 |
|
uhgrwkspthlem2 |
|- ( ( F ( Walks ` G ) P /\ ( ( # ` F ) = 1 /\ A =/= B ) /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> Fun `' P ) |
17 |
1 12 15 16
|
syl3anc |
|- ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> Fun `' P ) |
18 |
|
isspth |
|- ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) ) |
19 |
10 17 18
|
sylanbrc |
|- ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> F ( SPaths ` G ) P ) |
20 |
|
3anass |
|- ( ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) <-> ( F ( SPaths ` G ) P /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) ) |
21 |
19 15 20
|
sylanbrc |
|- ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) |
22 |
|
3simpa |
|- ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) ) |
23 |
22
|
adantr |
|- ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) ) |
24 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
25 |
24
|
isspthonpth |
|- ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) ) |
26 |
23 25
|
syl |
|- ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> ( F ( A ( SPathsOn ` G ) B ) P <-> ( F ( SPaths ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) ) |
27 |
21 26
|
mpbird |
|- ( ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) ) -> F ( A ( SPathsOn ` G ) B ) P ) |
28 |
27
|
ex |
|- ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> F ( A ( SPathsOn ` G ) B ) P ) ) |
29 |
24
|
wlkonprop |
|- ( F ( A ( WalksOn ` G ) B ) P -> ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) ) |
30 |
|
3simpc |
|- ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) ) |
31 |
30
|
3anim1i |
|- ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) ) |
32 |
29 31
|
syl |
|- ( F ( A ( WalksOn ` G ) B ) P -> ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) ) |
33 |
28 32
|
syl11 |
|- ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( F ( A ( WalksOn ` G ) B ) P -> F ( A ( SPathsOn ` G ) B ) P ) ) |
34 |
|
spthonpthon |
|- ( F ( A ( SPathsOn ` G ) B ) P -> F ( A ( PathsOn ` G ) B ) P ) |
35 |
|
pthontrlon |
|- ( F ( A ( PathsOn ` G ) B ) P -> F ( A ( TrailsOn ` G ) B ) P ) |
36 |
|
trlsonwlkon |
|- ( F ( A ( TrailsOn ` G ) B ) P -> F ( A ( WalksOn ` G ) B ) P ) |
37 |
34 35 36
|
3syl |
|- ( F ( A ( SPathsOn ` G ) B ) P -> F ( A ( WalksOn ` G ) B ) P ) |
38 |
33 37
|
impbid1 |
|- ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( F ( A ( WalksOn ` G ) B ) P <-> F ( A ( SPathsOn ` G ) B ) P ) ) |