Metamath Proof Explorer

Theorem usgr2pthlem

Description: Lemma for usgr2pth . (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 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 } ) ) ) )

Proof

Step Hyp Ref Expression
1 usgr2pthlem.v 
 |-  V = ( Vtx ` G )
2 usgr2pthlem.i 
 |-  I = ( iEdg ` G )
3 0nn0 
 |-  0 e. NN0
4 2nn0 
 |-  2 e. NN0
5 0le2 
 |-  0 <_ 2
6 elfz2nn0 
 |-  ( 0 e. ( 0 ... 2 ) <-> ( 0 e. NN0 /\ 2 e. NN0 /\ 0 <_ 2 ) )
7 3 4 5 6 mpbir3an 
 |-  0 e. ( 0 ... 2 )
8 ffvelcdm 
 |-  ( ( P : ( 0 ... 2 ) --> V /\ 0 e. ( 0 ... 2 ) ) -> ( P ` 0 ) e. V )
9 7 8 mpan2 
 |-  ( P : ( 0 ... 2 ) --> V -> ( P ` 0 ) e. V )
10 9 adantl 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( P ` 0 ) e. V )
11 1nn0 
 |-  1 e. NN0
12 1le2 
 |-  1 <_ 2
13 elfz2nn0 
 |-  ( 1 e. ( 0 ... 2 ) <-> ( 1 e. NN0 /\ 2 e. NN0 /\ 1 <_ 2 ) )
14 11 4 12 13 mpbir3an 
 |-  1 e. ( 0 ... 2 )
15 ffvelcdm 
 |-  ( ( P : ( 0 ... 2 ) --> V /\ 1 e. ( 0 ... 2 ) ) -> ( P ` 1 ) e. V )
16 14 15 mpan2 
 |-  ( P : ( 0 ... 2 ) --> V -> ( P ` 1 ) e. V )
17 16 adantl 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( P ` 1 ) e. V )
18 simpr 
 |-  ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) -> G e. USGraph )
19 fvex 
 |-  ( P ` 1 ) e. _V
20 18 19 jctir 
 |-  ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) -> ( G e. USGraph /\ ( P ` 1 ) e. _V ) )
21 prcom 
 |-  { ( P ` 0 ) , ( P ` 1 ) } = { ( P ` 1 ) , ( P ` 0 ) }
22 21 eqeq2i 
 |-  ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } <-> ( I ` ( F ` 0 ) ) = { ( P ` 1 ) , ( P ` 0 ) } )
23 22 birani 
 |-  ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( I ` ( F ` 0 ) ) = { ( P ` 1 ) , ( P ` 0 ) } )
24 23 ad2antlr 
 |-  ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) -> ( I ` ( F ` 0 ) ) = { ( P ` 1 ) , ( P ` 0 ) } )
25 2 usgrnloopv 
 |-  ( ( G e. USGraph /\ ( P ` 1 ) e. _V ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 1 ) , ( P ` 0 ) } -> ( P ` 1 ) =/= ( P ` 0 ) ) )
26 20 24 25 sylc 
 |-  ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) -> ( P ` 1 ) =/= ( P ` 0 ) )
27 26 adantr 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( P ` 1 ) =/= ( P ` 0 ) )
28 19 elsn 
 |-  ( ( P ` 1 ) e. { ( P ` 0 ) } <-> ( P ` 1 ) = ( P ` 0 ) )
29 28 necon3bbii 
 |-  ( -. ( P ` 1 ) e. { ( P ` 0 ) } <-> ( P ` 1 ) =/= ( P ` 0 ) )
30 27 29 sylibr 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> -. ( P ` 1 ) e. { ( P ` 0 ) } )
31 17 30 eldifd 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( P ` 1 ) e. ( V \ { ( P ` 0 ) } ) )
32 31 adantr 
 |-  ( ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) /\ x = ( P ` 0 ) ) -> ( P ` 1 ) e. ( V \ { ( P ` 0 ) } ) )
33 sneq 
 |-  ( x = ( P ` 0 ) -> { x } = { ( P ` 0 ) } )
34 33 difeq2d 
 |-  ( x = ( P ` 0 ) -> ( V \ { x } ) = ( V \ { ( P ` 0 ) } ) )
35 34 eleq2d 
 |-  ( x = ( P ` 0 ) -> ( ( P ` 1 ) e. ( V \ { x } ) <-> ( P ` 1 ) e. ( V \ { ( P ` 0 ) } ) ) )
36 35 adantl 
 |-  ( ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) /\ x = ( P ` 0 ) ) -> ( ( P ` 1 ) e. ( V \ { x } ) <-> ( P ` 1 ) e. ( V \ { ( P ` 0 ) } ) ) )
37 32 36 mpbird 
 |-  ( ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) /\ x = ( P ` 0 ) ) -> ( P ` 1 ) e. ( V \ { x } ) )
38 2re 
 |-  2 e. RR
39 38 leidi 
 |-  2 <_ 2
40 elfz2nn0 
 |-  ( 2 e. ( 0 ... 2 ) <-> ( 2 e. NN0 /\ 2 e. NN0 /\ 2 <_ 2 ) )
41 4 4 39 40 mpbir3an 
 |-  2 e. ( 0 ... 2 )
42 ffvelcdm 
 |-  ( ( P : ( 0 ... 2 ) --> V /\ 2 e. ( 0 ... 2 ) ) -> ( P ` 2 ) e. V )
43 41 42 mpan2 
 |-  ( P : ( 0 ... 2 ) --> V -> ( P ` 2 ) e. V )
44 43 adantl 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( P ` 2 ) e. V )
45 2 usgrf1 
 |-  ( G e. USGraph -> I : dom I -1-1-> ran I )
46 45 ad2antlr 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> I : dom I -1-1-> ran I )
47 simpl 
 |-  ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) -> F : ( 0 ..^ 2 ) -1-1-> dom I )
48 47 ad2antrr 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> F : ( 0 ..^ 2 ) -1-1-> dom I )
49 46 48 jca 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( I : dom I -1-1-> ran I /\ F : ( 0 ..^ 2 ) -1-1-> dom I ) )
50 2nn 
 |-  2 e. NN
51 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 2 ) <-> 2 e. NN )
52 50 51 mpbir 
 |-  0 e. ( 0 ..^ 2 )
53 1lt2 
 |-  1 < 2
54 elfzo0 
 |-  ( 1 e. ( 0 ..^ 2 ) <-> ( 1 e. NN0 /\ 2 e. NN /\ 1 < 2 ) )
55 11 50 53 54 mpbir3an 
 |-  1 e. ( 0 ..^ 2 )
56 52 55 pm3.2i 
 |-  ( 0 e. ( 0 ..^ 2 ) /\ 1 e. ( 0 ..^ 2 ) )
57 56 a1i 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( 0 e. ( 0 ..^ 2 ) /\ 1 e. ( 0 ..^ 2 ) ) )
58 0ne1 
 |-  0 =/= 1
59 58 a1i 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> 0 =/= 1 )
60 49 57 59 3jca 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( ( I : dom I -1-1-> ran I /\ F : ( 0 ..^ 2 ) -1-1-> dom I ) /\ ( 0 e. ( 0 ..^ 2 ) /\ 1 e. ( 0 ..^ 2 ) ) /\ 0 =/= 1 ) )
61 simpr 
 |-  ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
62 61 ad2antrr 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
63 2f1fvneq 
 |-  ( ( ( I : dom I -1-1-> ran I /\ F : ( 0 ..^ 2 ) -1-1-> dom I ) /\ ( 0 e. ( 0 ..^ 2 ) /\ 1 e. ( 0 ..^ 2 ) ) /\ 0 =/= 1 ) -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> { ( P ` 0 ) , ( P ` 1 ) } =/= { ( P ` 1 ) , ( P ` 2 ) } ) )
64 60 62 63 sylc 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> { ( P ` 0 ) , ( P ` 1 ) } =/= { ( P ` 1 ) , ( P ` 2 ) } )
65 necom 
 |-  ( ( P ` 2 ) =/= ( P ` 0 ) <-> ( P ` 0 ) =/= ( P ` 2 ) )
66 fvex 
 |-  ( P ` 0 ) e. _V
67 fvex 
 |-  ( P ` 2 ) e. _V
68 66 19 67 3pm3.2i 
 |-  ( ( P ` 0 ) e. _V /\ ( P ` 1 ) e. _V /\ ( P ` 2 ) e. _V )
69 fvexd 
 |-  ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) -> ( P ` 0 ) e. _V )
70 simpl 
 |-  ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } )
71 70 ad2antlr 
 |-  ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) -> ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } )
72 18 69 71 jca31 
 |-  ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) -> ( ( G e. USGraph /\ ( P ` 0 ) e. _V ) /\ ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } ) )
73 72 adantr 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( ( G e. USGraph /\ ( P ` 0 ) e. _V ) /\ ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } ) )
74 2 usgrnloopv 
 |-  ( ( G e. USGraph /\ ( P ` 0 ) e. _V ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } -> ( P ` 0 ) =/= ( P ` 1 ) ) )
75 74 imp 
 |-  ( ( ( G e. USGraph /\ ( P ` 0 ) e. _V ) /\ ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } ) -> ( P ` 0 ) =/= ( P ` 1 ) )
76 73 75 syl 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( P ` 0 ) =/= ( P ` 1 ) )
77 pr1nebg 
 |-  ( ( ( ( P ` 0 ) e. _V /\ ( P ` 1 ) e. _V /\ ( P ` 2 ) e. _V ) /\ ( P ` 0 ) =/= ( P ` 1 ) ) -> ( ( P ` 0 ) =/= ( P ` 2 ) <-> { ( P ` 0 ) , ( P ` 1 ) } =/= { ( P ` 1 ) , ( P ` 2 ) } ) )
78 68 76 77 sylancr 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( ( P ` 0 ) =/= ( P ` 2 ) <-> { ( P ` 0 ) , ( P ` 1 ) } =/= { ( P ` 1 ) , ( P ` 2 ) } ) )
79 65 78 bitrid 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( ( P ` 2 ) =/= ( P ` 0 ) <-> { ( P ` 0 ) , ( P ` 1 ) } =/= { ( P ` 1 ) , ( P ` 2 ) } ) )
80 64 79 mpbird 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( P ` 2 ) =/= ( P ` 0 ) )
81 fvexd 
 |-  ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) -> ( P ` 2 ) e. _V )
82 prcom 
 |-  { ( P ` 1 ) , ( P ` 2 ) } = { ( P ` 2 ) , ( P ` 1 ) }
83 82 eqeq2i 
 |-  ( ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } <-> ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } )
84 83 bilani 
 |-  ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } )
85 84 ad2antlr 
 |-  ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) -> ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } )
86 18 81 85 jca31 
 |-  ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) -> ( ( G e. USGraph /\ ( P ` 2 ) e. _V ) /\ ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } ) )
87 86 adantr 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( ( G e. USGraph /\ ( P ` 2 ) e. _V ) /\ ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } ) )
88 2 usgrnloopv 
 |-  ( ( G e. USGraph /\ ( P ` 2 ) e. _V ) -> ( ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } -> ( P ` 2 ) =/= ( P ` 1 ) ) )
89 88 imp 
 |-  ( ( ( G e. USGraph /\ ( P ` 2 ) e. _V ) /\ ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } ) -> ( P ` 2 ) =/= ( P ` 1 ) )
90 87 89 syl 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( P ` 2 ) =/= ( P ` 1 ) )
91 80 90 nelprd 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> -. ( P ` 2 ) e. { ( P ` 0 ) , ( P ` 1 ) } )
92 44 91 eldifd 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( P ` 2 ) e. ( V \ { ( P ` 0 ) , ( P ` 1 ) } ) )
93 92 ad2antrr 
 |-  ( ( ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) /\ x = ( P ` 0 ) ) /\ y = ( P ` 1 ) ) -> ( P ` 2 ) e. ( V \ { ( P ` 0 ) , ( P ` 1 ) } ) )
94 preq12 
 |-  ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) -> { x , y } = { ( P ` 0 ) , ( P ` 1 ) } )
95 94 difeq2d 
 |-  ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) -> ( V \ { x , y } ) = ( V \ { ( P ` 0 ) , ( P ` 1 ) } ) )
96 95 eleq2d 
 |-  ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) -> ( ( P ` 2 ) e. ( V \ { x , y } ) <-> ( P ` 2 ) e. ( V \ { ( P ` 0 ) , ( P ` 1 ) } ) ) )
97 96 adantll 
 |-  ( ( ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) /\ x = ( P ` 0 ) ) /\ y = ( P ` 1 ) ) -> ( ( P ` 2 ) e. ( V \ { x , y } ) <-> ( P ` 2 ) e. ( V \ { ( P ` 0 ) , ( P ` 1 ) } ) ) )
98 93 97 mpbird 
 |-  ( ( ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) /\ x = ( P ` 0 ) ) /\ y = ( P ` 1 ) ) -> ( P ` 2 ) e. ( V \ { x , y } ) )
99 eqcom 
 |-  ( x = ( P ` 0 ) <-> ( P ` 0 ) = x )
100 eqcom 
 |-  ( y = ( P ` 1 ) <-> ( P ` 1 ) = y )
101 eqcom 
 |-  ( z = ( P ` 2 ) <-> ( P ` 2 ) = z )
102 99 100 101 3anbi123i 
 |-  ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) /\ z = ( P ` 2 ) ) <-> ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) )
103 102 biimpi 
 |-  ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) /\ z = ( P ` 2 ) ) -> ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) )
104 103 ad4ant123 
 |-  ( ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) -> ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) )
105 99 biimpi 
 |-  ( x = ( P ` 0 ) -> ( P ` 0 ) = x )
106 105 ad2antrr 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( P ` 0 ) = x )
107 100 biimpi 
 |-  ( y = ( P ` 1 ) -> ( P ` 1 ) = y )
108 107 ad2antlr 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( P ` 1 ) = y )
109 106 108 preq12d 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> { ( P ` 0 ) , ( P ` 1 ) } = { x , y } )
110 109 eqeq2d 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } <-> ( I ` ( F ` 0 ) ) = { x , y } ) )
111 101 bilani 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( P ` 2 ) = z )
112 108 111 preq12d 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> { ( P ` 1 ) , ( P ` 2 ) } = { y , z } )
113 112 eqeq2d 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } <-> ( I ` ( F ` 1 ) ) = { y , z } ) )
114 110 113 anbi12d 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) <-> ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) )
115 114 biimpa 
 |-  ( ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) -> ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) )
116 104 115 jca 
 |-  ( ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) -> ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) )
117 116 exp41 
 |-  ( x = ( P ` 0 ) -> ( y = ( P ` 1 ) -> ( z = ( P ` 2 ) -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) ) )
118 117 adantl 
 |-  ( ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) /\ x = ( P ` 0 ) ) -> ( y = ( P ` 1 ) -> ( z = ( P ` 2 ) -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) ) ) )
119 118 imp31 
 |-  ( ( ( ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) /\ x = ( P ` 0 ) ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) /\ ( ( I ` ( F ` 0 ) ) = { x , y } /\ ( I ` ( F ` 1 ) ) = { y , z } ) ) ) )
120 98 119 rspcimedv 
 |-  ( ( ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) /\ x = ( P ` 0 ) ) /\ y = ( P ` 1 ) ) -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> 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 } ) ) ) )
121 37 120 rspcimedv 
 |-  ( ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) /\ x = ( P ` 0 ) ) -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> 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 } ) ) ) )
122 10 121 rspcimedv 
 |-  ( ( ( ( F : ( 0 ..^ 2 ) -1-1-> dom I /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) /\ G e. USGraph ) /\ P : ( 0 ... 2 ) --> V ) -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 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 } ) ) ) )
123 122 exp41 
 |-  ( F : ( 0 ..^ 2 ) -1-1-> dom I -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( G e. USGraph -> ( P : ( 0 ... 2 ) --> V -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 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 } ) ) ) ) ) ) )
124 123 com15 
 |-  ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( G e. USGraph -> ( P : ( 0 ... 2 ) --> V -> ( F : ( 0 ..^ 2 ) -1-1-> dom I -> 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 } ) ) ) ) ) ) )
125 124 pm2.43i 
 |-  ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( G e. USGraph -> ( P : ( 0 ... 2 ) --> V -> ( F : ( 0 ..^ 2 ) -1-1-> dom I -> 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 } ) ) ) ) ) )
126 125 com12 
 |-  ( G e. USGraph -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P : ( 0 ... 2 ) --> V -> ( F : ( 0 ..^ 2 ) -1-1-> dom I -> 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 } ) ) ) ) ) )
127 126 adantr 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P : ( 0 ... 2 ) --> V -> ( F : ( 0 ..^ 2 ) -1-1-> dom I -> 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 } ) ) ) ) ) )
128 oveq2 
 |-  ( ( # ` F ) = 2 -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 2 ) )
129 128 raleqdv 
 |-  ( ( # ` F ) = 2 -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> A. i e. ( 0 ..^ 2 ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
130 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
131 130 raleqi 
 |-  ( A. i e. ( 0 ..^ 2 ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> A. i e. { 0 , 1 } ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
132 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 ) } ) )
133 131 132 bitri 
 |-  ( A. i e. ( 0 ..^ 2 ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
134 129 133 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 ) } ) ) )
135 134 adantl 
 |-  ( ( G e. USGraph /\ ( # ` 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 ) } ) ) )
136 oveq2 
 |-  ( ( # ` F ) = 2 -> ( 0 ... ( # ` F ) ) = ( 0 ... 2 ) )
137 136 feq2d 
 |-  ( ( # ` F ) = 2 -> ( P : ( 0 ... ( # ` F ) ) --> V <-> P : ( 0 ... 2 ) --> V ) )
138 137 adantl 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( P : ( 0 ... ( # ` F ) ) --> V <-> P : ( 0 ... 2 ) --> V ) )
139 f1eq2 
 |-  ( ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 2 ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> F : ( 0 ..^ 2 ) -1-1-> dom I ) )
140 128 139 syl 
 |-  ( ( # ` F ) = 2 -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> F : ( 0 ..^ 2 ) -1-1-> dom I ) )
141 140 imbi1d 
 |-  ( ( # ` F ) = 2 -> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> 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 : ( 0 ..^ 2 ) -1-1-> dom I -> 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 } ) ) ) ) )
142 141 adantl 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> 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 : ( 0 ..^ 2 ) -1-1-> dom I -> 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 } ) ) ) ) )
143 138 142 imbi12d 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( P : ( 0 ... ( # ` F ) ) --> V -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> 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 } ) ) ) ) <-> ( P : ( 0 ... 2 ) --> V -> ( F : ( 0 ..^ 2 ) -1-1-> dom I -> 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 } ) ) ) ) ) )
144 127 135 143 3imtr4d 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( P : ( 0 ... ( # ` F ) ) --> V -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> 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 } ) ) ) ) ) )
145 144 com14 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( P : ( 0 ... ( # ` F ) ) --> V -> ( ( 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 } ) ) ) ) ) )
146 145 com23 
 |-  ( 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 } ) ) ) ) ) )
147 146 3imp 
 |-  ( ( 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 } ) ) ) )