Metamath Proof Explorer


Theorem usgr2pth

Description: In a simple 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) (Proof shortened by AV, 31-Oct-2021)

Ref Expression
Hypotheses usgr2pthlem.v
|- V = ( Vtx ` G )
usgr2pthlem.i
|- I = ( iEdg ` G )
Assertion 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. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 usgr2pthlem.v
 |-  V = ( Vtx ` G )
2 usgr2pthlem.i
 |-  I = ( iEdg ` G )
3 usgr2pthspth
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Paths ` G ) P <-> F ( SPaths ` G ) P ) )
4 usgrupgr
 |-  ( G e. USGraph -> G e. UPGraph )
5 4 adantr
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> G e. UPGraph )
6 isspth
 |-  ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )
7 6 a1i
 |-  ( G e. UPGraph -> ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) ) )
8 1 2 upgrf1istrl
 |-  ( G e. UPGraph -> ( F ( Trails ` G ) P <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
9 8 anbi1d
 |-  ( G e. UPGraph -> ( ( F ( Trails ` G ) P /\ Fun `' P ) <-> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ Fun `' P ) ) )
10 oveq2
 |-  ( ( # ` F ) = 2 -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 2 ) )
11 f1eq2
 |-  ( ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 2 ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> F : ( 0 ..^ 2 ) -1-1-> dom I ) )
12 10 11 syl
 |-  ( ( # ` F ) = 2 -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> F : ( 0 ..^ 2 ) -1-1-> dom I ) )
13 12 biimpd
 |-  ( ( # ` F ) = 2 -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> F : ( 0 ..^ 2 ) -1-1-> dom I ) )
14 13 adantl
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> F : ( 0 ..^ 2 ) -1-1-> dom I ) )
15 14 com12
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> F : ( 0 ..^ 2 ) -1-1-> dom I ) )
16 15 3ad2ant1
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> F : ( 0 ..^ 2 ) -1-1-> dom I ) )
17 16 ad2antrl
 |-  ( ( G e. UPGraph /\ ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ Fun `' P ) ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> F : ( 0 ..^ 2 ) -1-1-> dom I ) )
18 oveq2
 |-  ( ( # ` F ) = 2 -> ( 0 ... ( # ` F ) ) = ( 0 ... 2 ) )
19 18 feq2d
 |-  ( ( # ` F ) = 2 -> ( P : ( 0 ... ( # ` F ) ) --> V <-> P : ( 0 ... 2 ) --> V ) )
20 df-f1
 |-  ( P : ( 0 ... 2 ) -1-1-> V <-> ( P : ( 0 ... 2 ) --> V /\ Fun `' P ) )
21 20 simplbi2
 |-  ( P : ( 0 ... 2 ) --> V -> ( Fun `' P -> P : ( 0 ... 2 ) -1-1-> V ) )
22 21 a1i
 |-  ( ( # ` F ) = 2 -> ( P : ( 0 ... 2 ) --> V -> ( Fun `' P -> P : ( 0 ... 2 ) -1-1-> V ) ) )
23 19 22 sylbid
 |-  ( ( # ` F ) = 2 -> ( P : ( 0 ... ( # ` F ) ) --> V -> ( Fun `' P -> P : ( 0 ... 2 ) -1-1-> V ) ) )
24 23 adantl
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( P : ( 0 ... ( # ` F ) ) --> V -> ( Fun `' P -> P : ( 0 ... 2 ) -1-1-> V ) ) )
25 24 com3l
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> ( Fun `' P -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> P : ( 0 ... 2 ) -1-1-> V ) ) )
26 25 3ad2ant2
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( Fun `' P -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> P : ( 0 ... 2 ) -1-1-> V ) ) )
27 26 imp
 |-  ( ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ Fun `' P ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> P : ( 0 ... 2 ) -1-1-> V ) )
28 27 adantl
 |-  ( ( G e. UPGraph /\ ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ Fun `' P ) ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> P : ( 0 ... 2 ) -1-1-> V ) )
29 1 2 usgr2pthlem
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) )
30 29 ad2antrl
 |-  ( ( G e. UPGraph /\ ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ Fun `' P ) ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) )
31 17 28 30 3jcad
 |-  ( ( G e. UPGraph /\ ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ Fun `' P ) ) -> ( ( G e. USGraph /\ ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) )
32 31 ex
 |-  ( G e. UPGraph -> ( ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ Fun `' P ) -> ( ( G e. USGraph /\ ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) ) )
33 9 32 sylbid
 |-  ( G e. UPGraph -> ( ( F ( Trails ` G ) P /\ Fun `' P ) -> ( ( G e. USGraph /\ ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) ) )
34 7 33 sylbid
 |-  ( G e. UPGraph -> ( F ( SPaths ` G ) P -> ( ( G e. USGraph /\ ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) ) )
35 34 com23
 |-  ( G e. UPGraph -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( SPaths ` G ) P -> ( 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) ) )
36 5 35 mpcom
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( SPaths ` G ) P -> ( 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) )
37 3 36 sylbid
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Paths ` G ) P -> ( 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) )
38 37 ex
 |-  ( G e. USGraph -> ( ( # ` F ) = 2 -> ( F ( Paths ` G ) P -> ( 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) ) )
39 38 impcomd
 |-  ( 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) )
40 2nn0
 |-  2 e. NN0
41 f1f
 |-  ( F : ( 0 ..^ 2 ) -1-1-> dom I -> F : ( 0 ..^ 2 ) --> dom I )
42 fnfzo0hash
 |-  ( ( 2 e. NN0 /\ F : ( 0 ..^ 2 ) --> dom I ) -> ( # ` F ) = 2 )
43 40 41 42 sylancr
 |-  ( F : ( 0 ..^ 2 ) -1-1-> dom I -> ( # ` F ) = 2 )
44 oveq2
 |-  ( 2 = ( # ` F ) -> ( 0 ..^ 2 ) = ( 0 ..^ ( # ` F ) ) )
45 44 eqcoms
 |-  ( ( # ` F ) = 2 -> ( 0 ..^ 2 ) = ( 0 ..^ ( # ` F ) ) )
46 f1eq2
 |-  ( ( 0 ..^ 2 ) = ( 0 ..^ ( # ` F ) ) -> ( F : ( 0 ..^ 2 ) -1-1-> dom I <-> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I ) )
47 45 46 syl
 |-  ( ( # ` F ) = 2 -> ( F : ( 0 ..^ 2 ) -1-1-> dom I <-> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I ) )
48 47 biimpd
 |-  ( ( # ` F ) = 2 -> ( F : ( 0 ..^ 2 ) -1-1-> dom I -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I ) )
49 48 imp
 |-  ( ( ( # ` F ) = 2 /\ F : ( 0 ..^ 2 ) -1-1-> dom I ) -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I )
50 49 adantr
 |-  ( ( ( ( # ` F ) = 2 /\ F : ( 0 ..^ 2 ) -1-1-> dom I ) /\ P : ( 0 ... 2 ) -1-1-> V ) -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I )
51 50 ad2antrr
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I )
52 f1f
 |-  ( P : ( 0 ... 2 ) -1-1-> V -> P : ( 0 ... 2 ) --> V )
53 oveq2
 |-  ( 2 = ( # ` F ) -> ( 0 ... 2 ) = ( 0 ... ( # ` F ) ) )
54 53 eqcoms
 |-  ( ( # ` F ) = 2 -> ( 0 ... 2 ) = ( 0 ... ( # ` F ) ) )
55 54 adantr
 |-  ( ( ( # ` F ) = 2 /\ F : ( 0 ..^ 2 ) -1-1-> dom I ) -> ( 0 ... 2 ) = ( 0 ... ( # ` F ) ) )
56 55 feq2d
 |-  ( ( ( # ` F ) = 2 /\ F : ( 0 ..^ 2 ) -1-1-> dom I ) -> ( P : ( 0 ... 2 ) --> V <-> P : ( 0 ... ( # ` F ) ) --> V ) )
57 52 56 syl5ib
 |-  ( ( ( # ` F ) = 2 /\ F : ( 0 ..^ 2 ) -1-1-> dom I ) -> ( P : ( 0 ... 2 ) -1-1-> V -> P : ( 0 ... ( # ` F ) ) --> V ) )
58 57 imp
 |-  ( ( ( ( # ` F ) = 2 /\ F : ( 0 ..^ 2 ) -1-1-> dom I ) /\ P : ( 0 ... 2 ) -1-1-> V ) -> P : ( 0 ... ( # ` F ) ) --> V )
59 58 ad2antrr
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> P : ( 0 ... ( # ` F ) ) --> V )
60 eqcom
 |-  ( ( P ` 0 ) = x <-> x = ( P ` 0 ) )
61 60 biimpi
 |-  ( ( P ` 0 ) = x -> x = ( P ` 0 ) )
62 61 3ad2ant1
 |-  ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) -> x = ( P ` 0 ) )
63 eqcom
 |-  ( ( P ` 1 ) = y <-> y = ( P ` 1 ) )
64 63 biimpi
 |-  ( ( P ` 1 ) = y -> y = ( P ` 1 ) )
65 64 3ad2ant2
 |-  ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) -> y = ( P ` 1 ) )
66 62 65 preq12d
 |-  ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) -> { x , y } = { ( P ` 0 ) , ( P ` 1 ) } )
67 66 eqeq2d
 |-  ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) -> ( ( I ` ( F ` 0 ) ) = { x , y } <-> ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } ) )
68 67 biimpcd
 |-  ( ( I ` ( F ` 0 ) ) = { x , y } -> ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) -> ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } ) )
69 68 adantr
 |-  ( ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) -> ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) -> ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } ) )
70 69 impcom
 |-  ( ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) -> ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } )
71 eqcom
 |-  ( ( P ` 2 ) = z <-> z = ( P ` 2 ) )
72 71 biimpi
 |-  ( ( P ` 2 ) = z -> z = ( P ` 2 ) )
73 72 3ad2ant3
 |-  ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) -> z = ( P ` 2 ) )
74 65 73 preq12d
 |-  ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) -> { y , z } = { ( P ` 1 ) , ( P ` 2 ) } )
75 74 eqeq2d
 |-  ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) -> ( ( I ` ( F ` 1 ) ) = { y , z } <-> ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
76 75 biimpcd
 |-  ( ( I ` ( F ` 1 ) ) = { y , z } -> ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) -> ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
77 76 adantl
 |-  ( ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) -> ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) -> ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
78 77 impcom
 |-  ( ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) -> ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } )
79 70 78 jca
 |-  ( ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
80 79 rexlimivw
 |-  ( E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
81 80 rexlimivw
 |-  ( E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
82 81 rexlimivw
 |-  ( E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
83 82 a1i13
 |-  ( ( # ` F ) = 2 -> ( E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) -> ( G e. USGraph -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
84 fzo0to2pr
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
85 10 84 eqtrdi
 |-  ( ( # ` F ) = 2 -> ( 0 ..^ ( # ` F ) ) = { 0 , 1 } )
86 85 raleqdv
 |-  ( ( # ` F ) = 2 -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> A. i e. { 0 , 1 } ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
87 2wlklem
 |-  ( A. i e. { 0 , 1 } ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
88 86 87 bitrdi
 |-  ( ( # ` F ) = 2 -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) )
89 88 imbi2d
 |-  ( ( # ` F ) = 2 -> ( ( G e. USGraph -> A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) <-> ( G e. USGraph -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
90 83 89 sylibrd
 |-  ( ( # ` F ) = 2 -> ( E. x e. V E. y e. ( V \ { x } ) E. z e. ( V \ { x , y } ) ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) -> ( G e. USGraph -> A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
91 90 ad2antrr
 |-  ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) -> ( G e. USGraph -> A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
92 91 imp
 |-  ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) -> ( G e. USGraph -> A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
93 92 imp
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
94 51 59 93 3jca
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
95 20 simprbi
 |-  ( P : ( 0 ... 2 ) -1-1-> V -> Fun `' P )
96 95 adantl
 |-  ( ( ( ( # ` F ) = 2 /\ F : ( 0 ..^ 2 ) -1-1-> dom I ) /\ P : ( 0 ... 2 ) -1-1-> V ) -> Fun `' P )
97 96 ad2antrr
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> Fun `' P )
98 94 97 jca
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ Fun `' P ) )
99 7 9 bitrd
 |-  ( G e. UPGraph -> ( F ( SPaths ` G ) P <-> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ Fun `' P ) ) )
100 4 99 syl
 |-  ( G e. USGraph -> ( F ( SPaths ` G ) P <-> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ Fun `' P ) ) )
101 100 adantl
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> ( F ( SPaths ` G ) P <-> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ Fun `' P ) ) )
102 98 101 mpbird
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> F ( SPaths ` G ) P )
103 simpr
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> G e. USGraph )
104 simp-4l
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> ( # ` F ) = 2 )
105 103 104 3 syl2anc
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> ( F ( Paths ` G ) P <-> F ( SPaths ` G ) P ) )
106 102 105 mpbird
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> F ( Paths ` G ) P )
107 106 104 jca
 |-  ( ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) /\ G e. USGraph ) -> ( F ( Paths ` G ) P /\ ( # ` F ) = 2 ) )
108 107 ex
 |-  ( ( ( ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) -> ( G e. USGraph -> ( F ( Paths ` G ) P /\ ( # ` F ) = 2 ) ) )
109 108 exp41
 |-  ( ( # ` 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) -> ( G e. USGraph -> ( F ( Paths ` G ) P /\ ( # ` F ) = 2 ) ) ) ) ) )
110 43 109 mpcom
 |-  ( 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) -> ( G e. USGraph -> ( F ( Paths ` G ) P /\ ( # ` F ) = 2 ) ) ) ) )
111 110 3imp
 |-  ( ( 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) -> ( G e. USGraph -> ( F ( Paths ` G ) P /\ ( # ` F ) = 2 ) ) )
112 111 com12
 |-  ( G e. USGraph -> ( ( 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) -> ( F ( Paths ` G ) P /\ ( # ` F ) = 2 ) ) )
113 39 112 impbid
 |-  ( 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 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) )