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 biimpi 
 |-  ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } -> ( I ` ( F ` 0 ) ) = { ( P ` 1 ) , ( P ` 0 ) } )
24 23 adantr 
 |-  ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( I ` ( F ` 0 ) ) = { ( P ` 1 ) , ( P ` 0 ) } )
25 24 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 ) } )
26 2 usgrnloopv 
 |-  ( ( G e. USGraph /\ ( P ` 1 ) e. _V ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 1 ) , ( P ` 0 ) } -> ( P ` 1 ) =/= ( P ` 0 ) ) )
27 20 25 26 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 ) )
28 27 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 ) )
29 19 elsn 
 |-  ( ( P ` 1 ) e. { ( P ` 0 ) } <-> ( P ` 1 ) = ( P ` 0 ) )
30 29 necon3bbii 
 |-  ( -. ( P ` 1 ) e. { ( P ` 0 ) } <-> ( P ` 1 ) =/= ( P ` 0 ) )
31 28 30 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 ) } )
32 17 31 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 ) } ) )
33 32 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 ) } ) )
34 sneq 
 |-  ( x = ( P ` 0 ) -> { x } = { ( P ` 0 ) } )
35 34 difeq2d 
 |-  ( x = ( P ` 0 ) -> ( V \ { x } ) = ( V \ { ( P ` 0 ) } ) )
36 35 eleq2d 
 |-  ( x = ( P ` 0 ) -> ( ( P ` 1 ) e. ( V \ { x } ) <-> ( P ` 1 ) e. ( V \ { ( P ` 0 ) } ) ) )
37 36 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 ) } ) ) )
38 33 37 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 } ) )
39 2re 
 |-  2 e. RR
40 39 leidi 
 |-  2 <_ 2
41 elfz2nn0 
 |-  ( 2 e. ( 0 ... 2 ) <-> ( 2 e. NN0 /\ 2 e. NN0 /\ 2 <_ 2 ) )
42 4 4 40 41 mpbir3an 
 |-  2 e. ( 0 ... 2 )
43 ffvelcdm 
 |-  ( ( P : ( 0 ... 2 ) --> V /\ 2 e. ( 0 ... 2 ) ) -> ( P ` 2 ) e. V )
44 42 43 mpan2 
 |-  ( P : ( 0 ... 2 ) --> V -> ( P ` 2 ) e. V )
45 44 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 )
46 2 usgrf1 
 |-  ( G e. USGraph -> I : dom I -1-1-> ran I )
47 46 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 )
48 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 )
49 48 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 )
50 47 49 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 ) )
51 2nn 
 |-  2 e. NN
52 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 2 ) <-> 2 e. NN )
53 51 52 mpbir 
 |-  0 e. ( 0 ..^ 2 )
54 1lt2 
 |-  1 < 2
55 elfzo0 
 |-  ( 1 e. ( 0 ..^ 2 ) <-> ( 1 e. NN0 /\ 2 e. NN /\ 1 < 2 ) )
56 11 51 54 55 mpbir3an 
 |-  1 e. ( 0 ..^ 2 )
57 53 56 pm3.2i 
 |-  ( 0 e. ( 0 ..^ 2 ) /\ 1 e. ( 0 ..^ 2 ) )
58 57 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 ) ) )
59 0ne1 
 |-  0 =/= 1
60 59 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 )
61 50 58 60 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 ) )
62 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 ) } ) )
63 62 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 ) } ) )
64 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 ) } ) )
65 61 63 64 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 ) } )
66 necom 
 |-  ( ( P ` 2 ) =/= ( P ` 0 ) <-> ( P ` 0 ) =/= ( P ` 2 ) )
67 fvex 
 |-  ( P ` 0 ) e. _V
68 fvex 
 |-  ( P ` 2 ) e. _V
69 67 19 68 3pm3.2i 
 |-  ( ( P ` 0 ) e. _V /\ ( P ` 1 ) e. _V /\ ( P ` 2 ) e. _V )
70 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 )
71 simpl 
 |-  ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } )
72 71 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 ) } )
73 18 70 72 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 ) } ) )
74 73 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 ) } ) )
75 2 usgrnloopv 
 |-  ( ( G e. USGraph /\ ( P ` 0 ) e. _V ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } -> ( P ` 0 ) =/= ( P ` 1 ) ) )
76 75 imp 
 |-  ( ( ( G e. USGraph /\ ( P ` 0 ) e. _V ) /\ ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } ) -> ( P ` 0 ) =/= ( P ` 1 ) )
77 74 76 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 ) )
78 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 ) } ) )
79 69 77 78 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 ) } ) )
80 66 79 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 ) } ) )
81 65 80 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 ) )
82 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 )
83 prcom 
 |-  { ( P ` 1 ) , ( P ` 2 ) } = { ( P ` 2 ) , ( P ` 1 ) }
84 83 eqeq2i 
 |-  ( ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } <-> ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } )
85 84 biimpi 
 |-  ( ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } -> ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } )
86 85 adantl 
 |-  ( ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } )
87 86 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 ) } )
88 18 82 87 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 ) } ) )
89 88 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 ) } ) )
90 2 usgrnloopv 
 |-  ( ( G e. USGraph /\ ( P ` 2 ) e. _V ) -> ( ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } -> ( P ` 2 ) =/= ( P ` 1 ) ) )
91 90 imp 
 |-  ( ( ( G e. USGraph /\ ( P ` 2 ) e. _V ) /\ ( I ` ( F ` 1 ) ) = { ( P ` 2 ) , ( P ` 1 ) } ) -> ( P ` 2 ) =/= ( P ` 1 ) )
92 89 91 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 ) )
93 81 92 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 ) } )
94 45 93 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 ) } ) )
95 94 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 ) } ) )
96 preq12 
 |-  ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) -> { x , y } = { ( P ` 0 ) , ( P ` 1 ) } )
97 96 difeq2d 
 |-  ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) -> ( V \ { x , y } ) = ( V \ { ( P ` 0 ) , ( P ` 1 ) } ) )
98 97 eleq2d 
 |-  ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) -> ( ( P ` 2 ) e. ( V \ { x , y } ) <-> ( P ` 2 ) e. ( V \ { ( P ` 0 ) , ( P ` 1 ) } ) ) )
99 98 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 ) } ) ) )
100 95 99 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 } ) )
101 eqcom 
 |-  ( x = ( P ` 0 ) <-> ( P ` 0 ) = x )
102 eqcom 
 |-  ( y = ( P ` 1 ) <-> ( P ` 1 ) = y )
103 eqcom 
 |-  ( z = ( P ` 2 ) <-> ( P ` 2 ) = z )
104 101 102 103 3anbi123i 
 |-  ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) /\ z = ( P ` 2 ) ) <-> ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) )
105 104 biimpi 
 |-  ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) /\ z = ( P ` 2 ) ) -> ( ( P ` 0 ) = x /\ ( P ` 1 ) = y /\ ( P ` 2 ) = z ) )
106 105 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 ) )
107 101 biimpi 
 |-  ( x = ( P ` 0 ) -> ( P ` 0 ) = x )
108 107 ad2antrr 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( P ` 0 ) = x )
109 102 biimpi 
 |-  ( y = ( P ` 1 ) -> ( P ` 1 ) = y )
110 109 ad2antlr 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( P ` 1 ) = y )
111 108 110 preq12d 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> { ( P ` 0 ) , ( P ` 1 ) } = { x , y } )
112 111 eqeq2d 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } <-> ( I ` ( F ` 0 ) ) = { x , y } ) )
113 103 biimpi 
 |-  ( z = ( P ` 2 ) -> ( P ` 2 ) = z )
114 113 adantl 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( P ` 2 ) = z )
115 110 114 preq12d 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> { ( P ` 1 ) , ( P ` 2 ) } = { y , z } )
116 115 eqeq2d 
 |-  ( ( ( x = ( P ` 0 ) /\ y = ( P ` 1 ) ) /\ z = ( P ` 2 ) ) -> ( ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } <-> ( I ` ( F ` 1 ) ) = { y , z } ) )
117 112 116 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 } ) ) )
118 117 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 } ) )
119 106 118 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 } ) ) )
120 119 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 } ) ) ) ) ) )
121 120 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 } ) ) ) ) ) )
122 121 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 } ) ) ) )
123 100 122 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 } ) ) ) )
124 38 123 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 } ) ) ) )
125 10 124 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 } ) ) ) )
126 125 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 } ) ) ) ) ) ) )
127 126 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 } ) ) ) ) ) ) )
128 127 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 } ) ) ) ) ) )
129 128 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 } ) ) ) ) ) )
130 129 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 } ) ) ) ) ) )
131 oveq2 
 |-  ( ( # ` F ) = 2 -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 2 ) )
132 131 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 ) ) } ) )
133 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
134 133 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 ) ) } )
135 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 ) } ) )
136 134 135 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 ) } ) )
137 132 136 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 ) } ) ) )
138 137 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 ) } ) ) )
139 oveq2 
 |-  ( ( # ` F ) = 2 -> ( 0 ... ( # ` F ) ) = ( 0 ... 2 ) )
140 139 feq2d 
 |-  ( ( # ` F ) = 2 -> ( P : ( 0 ... ( # ` F ) ) --> V <-> P : ( 0 ... 2 ) --> V ) )
141 140 adantl 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( P : ( 0 ... ( # ` F ) ) --> V <-> P : ( 0 ... 2 ) --> V ) )
142 f1eq2 
 |-  ( ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 2 ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> F : ( 0 ..^ 2 ) -1-1-> dom I ) )
143 131 142 syl 
 |-  ( ( # ` F ) = 2 -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> F : ( 0 ..^ 2 ) -1-1-> dom I ) )
144 143 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 } ) ) ) ) )
145 144 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 } ) ) ) ) )
146 141 145 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 } ) ) ) ) ) )
147 130 138 146 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 } ) ) ) ) ) )
148 147 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 } ) ) ) ) ) )
149 148 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 } ) ) ) ) ) )
150 149 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 } ) ) ) )