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)

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 usgrupgr 
 |-  ( G e. USGraph -> G e. UPGraph )
4 3 adantr 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> G e. UPGraph )
5 simpl 
 |-  ( ( A e. V /\ C e. V ) -> A e. V )
6 5 adantl 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> A e. V )
7 simpr 
 |-  ( ( A e. V /\ C e. V ) -> C e. V )
8 7 adantl 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> C e. V )
9 1 elwspths2on 
 |-  ( ( G e. UPGraph /\ 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 ) ) ) )
10 4 6 8 9 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 ) ) ) )
11 simpl 
 |-  ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) -> G e. USGraph )
12 11 adantr 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) /\ b e. V ) -> G e. USGraph )
13 simplrl 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) /\ b e. V ) -> A e. V )
14 simpr 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) /\ b e. V ) -> b e. V )
15 simplrr 
 |-  ( ( ( G e. USGraph /\ ( A e. V /\ C e. V ) ) /\ b e. V ) -> C e. V )
16 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 ) ) )
17 12 13 14 15 16 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 ) ) )
18 17 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 ) ) ) )
19 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 ) ) ) )
20 3anass 
 |-  ( ( A =/= C /\ { A , b } e. E /\ { b , C } e. E ) <-> ( A =/= C /\ ( { A , b } e. E /\ { b , C } e. E ) ) )
21 20 bicomi 
 |-  ( ( A =/= C /\ ( { A , b } e. E /\ { b , C } e. E ) ) <-> ( A =/= C /\ { A , b } e. E /\ { b , C } e. E ) )
22 21 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 ) ) )
23 19 22 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 ) ) )
24 18 23 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 ) ) ) )
25 24 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 ) ) ) )
26 10 25 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 ) ) ) )