Metamath Proof Explorer

Theorem s3wwlks2on

Description: A length 3 string which represents a walk of length 2 between two vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021)

Ref Expression
Hypothesis s3wwlks2on.v 
|- V = ( Vtx ` G )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 s3wwlks2on.v 
 |-  V = ( Vtx ` G )
2 wwlknon 
 |-  ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> ( <" A B C "> e. ( 2 WWalksN G ) /\ ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) )
3 2 a1i 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> ( <" A B C "> e. ( 2 WWalksN G ) /\ ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) ) )
4 3anass 
 |-  ( ( <" A B C "> e. ( 2 WWalksN G ) /\ ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) <-> ( <" A B C "> e. ( 2 WWalksN G ) /\ ( ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) ) )
5 s3fv0 
 |-  ( A e. V -> ( <" A B C "> ` 0 ) = A )
6 s3fv2 
 |-  ( C e. V -> ( <" A B C "> ` 2 ) = C )
7 5 6 anim12i 
 |-  ( ( A e. V /\ C e. V ) -> ( ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) )
8 7 3adant1 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) )
9 8 biantrud 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( <" A B C "> e. ( 2 WWalksN G ) <-> ( <" A B C "> e. ( 2 WWalksN G ) /\ ( ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) ) ) )
10 4 9 bitr4id 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( ( <" A B C "> e. ( 2 WWalksN G ) /\ ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) <-> <" A B C "> e. ( 2 WWalksN G ) ) )
11 wlklnwwlknupgr 
 |-  ( G e. UPGraph -> ( E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) <-> <" A B C "> e. ( 2 WWalksN G ) ) )
12 11 bicomd 
 |-  ( G e. UPGraph -> ( <" A B C "> e. ( 2 WWalksN G ) <-> E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) )
13 12 3ad2ant1 
 |-  ( ( G e. UPGraph /\ A e. V /\ C e. V ) -> ( <" A B C "> e. ( 2 WWalksN G ) <-> E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) )
14 3 10 13 3bitrd 
 |-  ( ( 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 ) ) )