Step |
Hyp |
Ref |
Expression |
1 |
|
wlkson.v |
|- V = ( Vtx ` G ) |
2 |
1
|
wlkson |
|- ( ( A e. V /\ B e. V ) -> ( A ( WalksOn ` G ) B ) = { <. f , p >. | ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) } ) |
3 |
|
fveq1 |
|- ( p = P -> ( p ` 0 ) = ( P ` 0 ) ) |
4 |
3
|
adantl |
|- ( ( f = F /\ p = P ) -> ( p ` 0 ) = ( P ` 0 ) ) |
5 |
4
|
eqeq1d |
|- ( ( f = F /\ p = P ) -> ( ( p ` 0 ) = A <-> ( P ` 0 ) = A ) ) |
6 |
|
simpr |
|- ( ( f = F /\ p = P ) -> p = P ) |
7 |
|
fveq2 |
|- ( f = F -> ( # ` f ) = ( # ` F ) ) |
8 |
7
|
adantr |
|- ( ( f = F /\ p = P ) -> ( # ` f ) = ( # ` F ) ) |
9 |
6 8
|
fveq12d |
|- ( ( f = F /\ p = P ) -> ( p ` ( # ` f ) ) = ( P ` ( # ` F ) ) ) |
10 |
9
|
eqeq1d |
|- ( ( f = F /\ p = P ) -> ( ( p ` ( # ` f ) ) = B <-> ( P ` ( # ` F ) ) = B ) ) |
11 |
2 5 10
|
2rbropap |
|- ( ( ( A e. V /\ B e. V ) /\ F e. U /\ P e. Z ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) ) |
12 |
11
|
3expb |
|- ( ( ( A e. V /\ B e. V ) /\ ( F e. U /\ P e. Z ) ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) ) |