Step |
Hyp |
Ref |
Expression |
1 |
|
elwwlks2on.v |
|- V = ( Vtx ` G ) |
2 |
1
|
elwwlks2ons3 |
|- ( W e. ( A ( 2 WWalksNOn G ) C ) <-> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) ) |
3 |
1
|
s3wwlks2on |
|- ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) <-> E. f ( f ( Walks ` G ) <" A b C "> /\ ( # ` f ) = 2 ) ) ) |
4 |
|
breq2 |
|- ( <" A b C "> = W -> ( f ( Walks ` G ) <" A b C "> <-> f ( Walks ` G ) W ) ) |
5 |
4
|
eqcoms |
|- ( W = <" A b C "> -> ( f ( Walks ` G ) <" A b C "> <-> f ( Walks ` G ) W ) ) |
6 |
5
|
anbi1d |
|- ( W = <" A b C "> -> ( ( f ( Walks ` G ) <" A b C "> /\ ( # ` f ) = 2 ) <-> ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) ) |
7 |
6
|
exbidv |
|- ( W = <" A b C "> -> ( E. f ( f ( Walks ` G ) <" A b C "> /\ ( # ` f ) = 2 ) <-> E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) ) |
8 |
3 7
|
sylan9bb |
|- ( ( ( G e. UPGraph /\ A e. V /\ C e. V ) /\ W = <" A b C "> ) -> ( <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) <-> E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) ) |
9 |
8
|
pm5.32da |
|- ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) <-> ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) ) ) |
10 |
9
|
rexbidv |
|- ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) <-> E. b e. V ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) ) ) |
11 |
2 10
|
syl5bb |
|- ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WWalksNOn G ) C ) <-> E. b e. V ( W = <" A b C "> /\ E. f ( f ( Walks ` G ) W /\ ( # ` f ) = 2 ) ) ) ) |