This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sps3wwlks2on

Description: A length 3 string which represents a walk of length 2 between two vertices. Concerns simple pseudographs, in contrast to s3wwlks2on and does not require the Axiom of Choice for its proof. (Contributed by Ender Ting, 28-Jan-2026)

Ref Expression
Hypothesis s3wwlks2on.v 
|- V = ( Vtx ` G )
Assertion sps3wwlks2on 
|- ( ( G e. USPGraph /\ 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. USPGraph /\ 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 biantrud 
 |-  ( ( 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 ) ) ) )
9 4 8 bitr4id 
 |-  ( ( 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 ) ) )
10 9 3adant1 
 |-  ( ( G e. USPGraph /\ 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 wlklnwwlkn 
 |-  ( G e. USPGraph -> ( E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) <-> <" A B C "> e. ( 2 WWalksN G ) ) )
12 11 bicomd 
 |-  ( G e. USPGraph -> ( <" A B C "> e. ( 2 WWalksN G ) <-> E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) )
13 12 3ad2ant1 
 |-  ( ( G e. USPGraph /\ 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. USPGraph /\ 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 ) ) )