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 ffvelrn
 |-  ( ( 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 ffvelrn
 |-  ( ( 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 ffvelrn
 |-  ( ( 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 syl5bb
 |-  ( ( ( ( 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 } ) ) ) )