This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid 
 |-  ( ( ( # ` 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 } ) ) ) ) )