Metamath Proof Explorer

Theorem usgr2pth0

Description: In a simply graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018) (Revised by AV, 5-Jun-2021)

Ref Expression
Hypotheses usgr2pthlem.v 
|- V = ( Vtx ` G )
usgr2pthlem.i 
|- I = ( iEdg ` G )
Assertion usgr2pth0 
|- ( G e. USGraph -> ( ( F ( Paths ` G ) P /\ ( # ` F ) = 2 ) <-> ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ P : ( 0 ... 2 ) -1-1-> V /\ E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 usgr2pthlem.v 
 |-  V = ( Vtx ` G )
2 usgr2pthlem.i 
 |-  I = ( iEdg ` G )
3 1 2 usgr2pth 
 |-  ( G e. USGraph -> ( ( F ( Paths ` G ) P /\ ( # ` F ) = 2 ) <-> ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ P : ( 0 ... 2 ) -1-1-> V /\ E. x e. V E. z e. ( V \ { x } ) E. y e. ( V \ { x , z } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
4 r19.42v 
 |-  ( E. y e. ( V \ { x , z } ) ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> ( z =/= x /\ E. y e. ( V \ { x , z } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) )
5 rexdifpr 
 |-  ( E. y e. ( V \ { x , z } ) ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> E. y e. V ( y =/= x /\ y =/= z /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
6 4 5 bitr3i 
 |-  ( ( z =/= x /\ E. y e. ( V \ { x , z } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> E. y e. V ( y =/= x /\ y =/= z /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
7 6 rexbii 
 |-  ( E. z e. V ( z =/= x /\ E. y e. ( V \ { x , z } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> E. z e. V E. y e. V ( y =/= x /\ y =/= z /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
8 rexcom 
 |-  ( E. z e. V E. y e. V ( y =/= x /\ y =/= z /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) <-> E. y e. V E. z e. V ( y =/= x /\ y =/= z /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
9 df-3an 
 |-  ( ( y =/= x /\ y =/= z /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) <-> ( ( y =/= x /\ y =/= z ) /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
10 anass 
 |-  ( ( ( ( y =/= x /\ y =/= z ) /\ z =/= x ) /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> ( ( y =/= x /\ y =/= z ) /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
11 anass 
 |-  ( ( ( ( z =/= x /\ z =/= y ) /\ y =/= x ) /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> ( ( z =/= x /\ z =/= y ) /\ ( y =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
12 anass 
 |-  ( ( ( y =/= x /\ y =/= z ) /\ z =/= x ) <-> ( y =/= x /\ ( y =/= z /\ z =/= x ) ) )
13 ancom 
 |-  ( ( y =/= x /\ ( y =/= z /\ z =/= x ) ) <-> ( ( y =/= z /\ z =/= x ) /\ y =/= x ) )
14 necom 
 |-  ( y =/= z <-> z =/= y )
15 14 anbi2ci 
 |-  ( ( y =/= z /\ z =/= x ) <-> ( z =/= x /\ z =/= y ) )
16 15 anbi1i 
 |-  ( ( ( y =/= z /\ z =/= x ) /\ y =/= x ) <-> ( ( z =/= x /\ z =/= y ) /\ y =/= x ) )
17 12 13 16 3bitri 
 |-  ( ( ( y =/= x /\ y =/= z ) /\ z =/= x ) <-> ( ( z =/= x /\ z =/= y ) /\ y =/= x ) )
18 17 anbi1i 
 |-  ( ( ( ( y =/= x /\ y =/= z ) /\ z =/= x ) /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> ( ( ( z =/= x /\ z =/= y ) /\ y =/= x ) /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) )
19 df-3an 
 |-  ( ( z =/= x /\ z =/= y /\ ( y =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) <-> ( ( z =/= x /\ z =/= y ) /\ ( y =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
20 11 18 19 3bitr4i 
 |-  ( ( ( ( y =/= x /\ y =/= z ) /\ z =/= x ) /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> ( z =/= x /\ z =/= y /\ ( y =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
21 9 10 20 3bitr2i 
 |-  ( ( y =/= x /\ y =/= z /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) <-> ( z =/= x /\ z =/= y /\ ( y =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
22 21 rexbii 
 |-  ( E. z e. V ( y =/= x /\ y =/= z /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) <-> E. z e. V ( z =/= x /\ z =/= y /\ ( y =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
23 rexdifpr 
 |-  ( E. z e. ( V \ { x , y } ) ( y =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> E. z e. V ( z =/= x /\ z =/= y /\ ( y =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
24 r19.42v 
 |-  ( E. z e. ( V \ { x , y } ) ( y =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> ( y =/= x /\ E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) )
25 22 23 24 3bitr2i 
 |-  ( E. z e. V ( y =/= x /\ y =/= z /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) <-> ( y =/= x /\ E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) )
26 25 rexbii 
 |-  ( E. y e. V E. z e. V ( y =/= x /\ y =/= z /\ ( z =/= x /\ ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) <-> E. y e. V ( y =/= x /\ E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) )
27 7 8 26 3bitri 
 |-  ( E. z e. V ( z =/= x /\ E. y e. ( V \ { x , z } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> E. y e. V ( y =/= x /\ E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) )
28 rexdifsn 
 |-  ( E. z e. ( V \ { x } ) E. y e. ( V \ { x , z } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) <-> E. z e. V ( z =/= x /\ E. y e. ( V \ { x , z } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) )
29 rexdifsn 
 |-  ( E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) <-> E. y e. V ( y =/= x /\ E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) )
30 27 28 29 3bitr4i 
 |-  ( E. z e. ( V \ { x } ) E. y e. ( V \ { x , z } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) <-> E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) )
31 30 a1i 
 |-  ( ( G e. USGraph /\ x e. V ) -> ( E. z e. ( V \ { x } ) E. y e. ( V \ { x , z } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) <-> E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) )
32 31 rexbidva 
 |-  ( G e. USGraph -> ( E. x e. V E. z e. ( V \ { x } ) E. y e. ( V \ { x , z } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) <-> E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) )
33 32 3anbi3d 
 |-  ( G e. USGraph -> ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ P : ( 0 ... 2 ) -1-1-> V /\ E. x e. V E. z e. ( V \ { x } ) E. y e. ( V \ { x , z } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) <-> ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ P : ( 0 ... 2 ) -1-1-> V /\ E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )
34 3 33 bitrd 
 |-  ( G e. USGraph -> ( ( F ( Paths ` G ) P /\ ( # ` F ) = 2 ) <-> ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ P : ( 0 ... 2 ) -1-1-> V /\ E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = z /\ ( P ` 2 ) = y ) /\ ( ( I ` ( F ` 0 ) ) = { x , z } /\ ( I ` ( F ` 1 ) ) = { z , y } ) ) ) ) )