Metamath Proof Explorer

Theorem elwspths2onw

Description: A simple path of length 2 between two vertices (in a simple pseudograph) as length 3 string. This theorem avoids the Axiom of Choice for its proof, at the cost of requiring a simple graph; the more general version is elwspths2on . (Contributed by Ender Ting, 29-Jan-2026)

Ref Expression
Hypothesis elwwlks2on.v 
|- V = ( Vtx ` G )
Assertion elwspths2onw 
|- ( ( G e. USPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) <-> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )

Proof

Step Hyp Ref Expression
1 elwwlks2on.v 
 |-  V = ( Vtx ` G )
2 wspthnon 
 |-  ( W e. ( A ( 2 WSPathsNOn G ) C ) <-> ( W e. ( A ( 2 WWalksNOn G ) C ) /\ E. b b ( A ( SPathsOn ` G ) C ) W ) )
3 2 biimpi 
 |-  ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( W e. ( A ( 2 WWalksNOn G ) C ) /\ E. b b ( A ( SPathsOn ` G ) C ) W ) )
4 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 ) ) )
5 4 a1i 
 |-  ( ( G e. USPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WWalksNOn G ) C ) <-> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) ) )
6 simpl 
 |-  ( ( W = <" A b C "> /\ W e. ( A ( 2 WSPathsNOn G ) C ) ) -> W = <" A b C "> )
7 eleq1 
 |-  ( W = <" A b C "> -> ( W e. ( A ( 2 WSPathsNOn G ) C ) <-> <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) )
8 7 biimpa 
 |-  ( ( W = <" A b C "> /\ W e. ( A ( 2 WSPathsNOn G ) C ) ) -> <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) )
9 6 8 jca 
 |-  ( ( W = <" A b C "> /\ W e. ( A ( 2 WSPathsNOn G ) C ) ) -> ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) )
10 9 ex 
 |-  ( W = <" A b C "> -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
11 10 adantr 
 |-  ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
12 11 com12 
 |-  ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
13 12 reximdv 
 |-  ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( 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 "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
14 13 a1i13 
 |-  ( ( G e. USPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( E. b b ( A ( SPathsOn ` G ) C ) W -> ( 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 "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) ) ) )
15 14 com24 
 |-  ( ( G e. USPGraph /\ 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 b ( A ( SPathsOn ` G ) C ) W -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) ) ) )
16 5 15 sylbid 
 |-  ( ( G e. USPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WWalksNOn G ) C ) -> ( E. b b ( A ( SPathsOn ` G ) C ) W -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) ) ) )
17 16 impd 
 |-  ( ( G e. USPGraph /\ A e. V /\ C e. V ) -> ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ E. b b ( A ( SPathsOn ` G ) C ) W ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) ) )
18 17 com23 
 |-  ( ( G e. USPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> ( ( W e. ( A ( 2 WWalksNOn G ) C ) /\ E. b b ( A ( SPathsOn ` G ) C ) W ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) ) )
19 3 18 mpdi 
 |-  ( ( G e. USPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) -> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
20 7 biimpar 
 |-  ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) -> W e. ( A ( 2 WSPathsNOn G ) C ) )
21 20 a1i 
 |-  ( ( ( G e. USPGraph /\ A e. V /\ C e. V ) /\ b e. V ) -> ( ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) -> W e. ( A ( 2 WSPathsNOn G ) C ) ) )
22 21 rexlimdva 
 |-  ( ( G e. USPGraph /\ A e. V /\ C e. V ) -> ( E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) -> W e. ( A ( 2 WSPathsNOn G ) C ) ) )
23 19 22 impbid 
 |-  ( ( G e. USPGraph /\ A e. V /\ C e. V ) -> ( W e. ( A ( 2 WSPathsNOn G ) C ) <-> E. b e. V ( W = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )