Metamath Proof Explorer

Theorem usgr2wspthon

Description: A simple path of length 2 between two vertices corresponds to two adjacent edges in a simple graph. (Contributed by Alexander van der Vekens, 9-Mar-2018) (Revised by AV, 17-May-2021) (Revised by Ender Ting, 29-Jan-2026)

Ref Expression
Hypotheses usgr2wspthon0.v 
|- V = ( Vtx ` G )
usgr2wspthon0.e 
|- E = ( Edg ` G )
Assertion usgr2wspthon 
|- ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> ( T e. ( A ( 2 WSPathsNOn G ) C ) <-> E. b e. V ( ( T = <" A b C "> /\ A =/= C ) /\ ( { A , b } e. E /\ { b , C } e. E ) ) ) )

Proof

Step Hyp Ref Expression
1 usgr2wspthon0.v 
 |-  V = ( Vtx ` G )
2 usgr2wspthon0.e 
 |-  E = ( Edg ` G )
3 usgruspgr 
 |-  ( G e. USGraph -> G e. USPGraph )
4 3 adantr 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> G e. USPGraph )
5 simprl 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> A e. V )
6 simprr 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> C e. V )
7 1 elwspths2onw 
 |-  ( ( G e. USPGraph /\ A e. V /\ C e. V ) -> ( T e. ( A ( 2 WSPathsNOn G ) C ) <-> E. b e. V ( T = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
8 4 5 6 7 syl3anc 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> ( T e. ( A ( 2 WSPathsNOn G ) C ) <-> E. b e. V ( T = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) ) )
9 simpl 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> G e. USGraph )
10 9 adantr 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) /\ b e. V ) -> G e. USGraph )
11 simplrl 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) /\ b e. V ) -> A e. V )
12 simpr 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) /\ b e. V ) -> b e. V )
13 simplrr 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) /\ b e. V ) -> C e. V )
14 1 2 usgr2wspthons3 
 |-  ( ( G e. USGraph /\ ( A e. V /\ b e. V /\ C e. V ) ) -> ( <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) <-> ( A =/= C /\ { A , b } e. E /\ { b , C } e. E ) ) )
15 10 11 12 13 14 syl13anc 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) /\ b e. V ) -> ( <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) <-> ( A =/= C /\ { A , b } e. E /\ { b , C } e. E ) ) )
16 15 anbi2d 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) /\ b e. V ) -> ( ( T = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) <-> ( T = <" A b C "> /\ ( A =/= C /\ { A , b } e. E /\ { b , C } e. E ) ) ) )
17 anass 
 |-  ( ( ( T = <" A b C "> /\ A =/= C ) /\ ( { A , b } e. E /\ { b , C } e. E ) ) <-> ( T = <" A b C "> /\ ( A =/= C /\ ( { A , b } e. E /\ { b , C } e. E ) ) ) )
18 3anass 
 |-  ( ( A =/= C /\ { A , b } e. E /\ { b , C } e. E ) <-> ( A =/= C /\ ( { A , b } e. E /\ { b , C } e. E ) ) )
19 18 bicomi 
 |-  ( ( A =/= C /\ ( { A , b } e. E /\ { b , C } e. E ) ) <-> ( A =/= C /\ { A , b } e. E /\ { b , C } e. E ) )
20 19 anbi2i 
 |-  ( ( T = <" A b C "> /\ ( A =/= C /\ ( { A , b } e. E /\ { b , C } e. E ) ) ) <-> ( T = <" A b C "> /\ ( A =/= C /\ { A , b } e. E /\ { b , C } e. E ) ) )
21 17 20 bitri 
 |-  ( ( ( T = <" A b C "> /\ A =/= C ) /\ ( { A , b } e. E /\ { b , C } e. E ) ) <-> ( T = <" A b C "> /\ ( A =/= C /\ { A , b } e. E /\ { b , C } e. E ) ) )
22 16 21 bitr4di 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) /\ b e. V ) -> ( ( T = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) <-> ( ( T = <" A b C "> /\ A =/= C ) /\ ( { A , b } e. E /\ { b , C } e. E ) ) ) )
23 22 rexbidva 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> ( E. b e. V ( T = <" A b C "> /\ <" A b C "> e. ( A ( 2 WSPathsNOn G ) C ) ) <-> E. b e. V ( ( T = <" A b C "> /\ A =/= C ) /\ ( { A , b } e. E /\ { b , C } e. E ) ) ) )
24 8 23 bitrd 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> ( T e. ( A ( 2 WSPathsNOn G ) C ) <-> E. b e. V ( ( T = <" A b C "> /\ A =/= C ) /\ ( { A , b } e. E /\ { b , C } e. E ) ) ) )