MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  usgrcyclnl2 Structured version   Unicode version

Theorem usgrcyclnl2 25255
Description: In an undirected simple graph (with no loops!) there are no cycles with length 2 (consisting of two edges ). (Contributed by Alexander van der Vekens, 9-Nov-2017.)
Assertion
Ref Expression
usgrcyclnl2  |-  ( ( V USGrph  E  /\  F ( V Cycles  E ) P )  ->  ( # `  F
)  =/=  2 )

Proof of Theorem usgrcyclnl2
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 cyclispth 25243 . . . 4  |-  ( F ( V Cycles  E ) P  ->  F ( V Paths  E ) P )
2 pthistrl 25188 . . . . 5  |-  ( F ( V Paths  E ) P  ->  F ( V Trails  E ) P )
3 cycliswlk 25246 . . . . . 6  |-  ( F ( V Cycles  E ) P  ->  F ( V Walks  E ) P )
4 wlkbprop 25137 . . . . . 6  |-  ( F ( V Walks  E ) P  ->  ( ( # `
 F )  e. 
NN0  /\  ( V  e.  _V  /\  E  e. 
_V )  /\  ( F  e.  _V  /\  P  e.  _V ) ) )
5 istrl2 25154 . . . . . . . 8  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V )
)  ->  ( F
( V Trails  E ) P 
<->  ( F : ( 0..^ ( # `  F
) ) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } ) ) )
6 pm3.2 448 . . . . . . . 8  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V )
)  ->  ( ( F : ( 0..^ (
# `  F )
) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } )  ->  (
( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  ( F : ( 0..^ ( # `  F
) ) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } ) ) ) )
75, 6sylbid 218 . . . . . . 7  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V )
)  ->  ( F
( V Trails  E ) P  ->  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V )
)  /\  ( F : ( 0..^ (
# `  F )
) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } ) ) ) )
873adant1 1023 . . . . . 6  |-  ( ( ( # `  F
)  e.  NN0  /\  ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V )
)  ->  ( F
( V Trails  E ) P  ->  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V )
)  /\  ( F : ( 0..^ (
# `  F )
) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } ) ) ) )
93, 4, 83syl 18 . . . . 5  |-  ( F ( V Cycles  E ) P  ->  ( F
( V Trails  E ) P  ->  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V )
)  /\  ( F : ( 0..^ (
# `  F )
) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } ) ) ) )
102, 9syl5com 31 . . . 4  |-  ( F ( V Paths  E ) P  ->  ( F
( V Cycles  E ) P  ->  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V )
)  /\  ( F : ( 0..^ (
# `  F )
) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } ) ) ) )
111, 10mpcom 37 . . 3  |-  ( F ( V Cycles  E ) P  ->  ( (
( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V )
)  /\  ( F : ( 0..^ (
# `  F )
) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } ) ) )
12 iscycl 25239 . . . . 5  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V )
)  ->  ( F
( V Cycles  E ) P 
<->  ( F ( V Paths 
E ) P  /\  ( P `  0 )  =  ( P `  ( # `  F ) ) ) ) )
1312adantr 466 . . . 4  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  ( F : ( 0..^ ( # `  F
) ) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } ) )  -> 
( F ( V Cycles  E ) P  <->  ( F
( V Paths  E ) P  /\  ( P ` 
0 )  =  ( P `  ( # `  F ) ) ) ) )
14 oveq2 6304 . . . . . . . . . . . . . 14  |-  ( (
# `  F )  =  2  ->  (
0..^ ( # `  F
) )  =  ( 0..^ 2 ) )
15 f1eq2 5783 . . . . . . . . . . . . . 14  |-  ( ( 0..^ ( # `  F
) )  =  ( 0..^ 2 )  -> 
( F : ( 0..^ ( # `  F
) ) -1-1-> dom  E  <->  F : ( 0..^ 2 ) -1-1-> dom  E ) )
1614, 15syl 17 . . . . . . . . . . . . 13  |-  ( (
# `  F )  =  2  ->  ( F : ( 0..^ (
# `  F )
) -1-1-> dom  E  <->  F :
( 0..^ 2 )
-1-1-> dom  E ) )
1714raleqdv 3029 . . . . . . . . . . . . 13  |-  ( (
# `  F )  =  2  ->  ( A. k  e.  (
0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) }  <->  A. k  e.  ( 0..^ 2 ) ( E `  ( F `
 k ) )  =  { ( P `
 k ) ,  ( P `  (
k  +  1 ) ) } ) )
1816, 17anbi12d 715 . . . . . . . . . . . 12  |-  ( (
# `  F )  =  2  ->  (
( F : ( 0..^ ( # `  F
) ) -1-1-> dom  E  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } )  <->  ( F : ( 0..^ 2 ) -1-1-> dom  E  /\  A. k  e.  ( 0..^ 2 ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } ) ) )
19 fveq2 5872 . . . . . . . . . . . . 13  |-  ( (
# `  F )  =  2  ->  ( P `  ( # `  F
) )  =  ( P `  2 ) )
2019eqeq2d 2434 . . . . . . . . . . . 12  |-  ( (
# `  F )  =  2  ->  (
( P `  0
)  =  ( P `
 ( # `  F
) )  <->  ( P `  0 )  =  ( P `  2
) ) )
2118, 20anbi12d 715 . . . . . . . . . . 11  |-  ( (
# `  F )  =  2  ->  (
( ( F :
( 0..^ ( # `  F ) ) -1-1-> dom  E  /\  A. k  e.  ( 0..^ ( # `  F ) ) ( E `  ( F `
 k ) )  =  { ( P `
 k ) ,  ( P `  (
k  +  1 ) ) } )  /\  ( P `  0 )  =  ( P `  ( # `  F ) ) )  <->  ( ( F : ( 0..^ 2 ) -1-1-> dom  E  /\  A. k  e.  ( 0..^ 2 ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } )  /\  ( P `  0 )  =  ( P ` 
2 ) ) ) )
2221anbi1d 709 . . . . . . . . . 10  |-  ( (
# `  F )  =  2  ->  (
( ( ( F : ( 0..^ (
# `  F )
) -1-1-> dom  E  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } )  /\  ( P `  0 )  =  ( P `  ( # `  F ) ) )  /\  V USGrph  E )  <->  ( ( ( F : ( 0..^ 2 ) -1-1-> dom  E  /\  A. k  e.  ( 0..^ 2 ) ( E `  ( F `
 k ) )  =  { ( P `
 k ) ,  ( P `  (
k  +  1 ) ) } )  /\  ( P `  0 )  =  ( P ` 
2 ) )  /\  V USGrph  E ) ) )
23 fzo0to2pr 11984 . . . . . . . . . . . . . 14  |-  ( 0..^ 2 )  =  {
0 ,  1 }
2423raleqi 3027 . . . . . . . . . . . . 13  |-  ( A. k  e.  ( 0..^ 2 ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) }  <->  A. k  e.  {
0 ,  1 }  ( E `  ( F `  k )
)  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } )
25 2wlklem 25180 . . . . . . . . . . . . . 14  |-  ( A. k  e.  { 0 ,  1 }  ( E `  ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) }  <->  ( ( E `
 ( F ` 
0 ) )  =  { ( P ` 
0 ) ,  ( P `  1 ) }  /\  ( E `
 ( F ` 
1 ) )  =  { ( P ` 
1 ) ,  ( P `  2 ) } ) )
26 prcom 4072 . . . . . . . . . . . . . . . . . . 19  |-  { ( P `  1 ) ,  ( P ` 
2 ) }  =  { ( P ` 
2 ) ,  ( P `  1 ) }
2726eqeq2i 2438 . . . . . . . . . . . . . . . . . 18  |-  ( ( E `  ( F `
 1 ) )  =  { ( P `
 1 ) ,  ( P `  2
) }  <->  ( E `  ( F `  1
) )  =  {
( P `  2
) ,  ( P `
 1 ) } )
28 preq1 4073 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( P `  2 )  =  ( P ` 
0 )  ->  { ( P `  2 ) ,  ( P ` 
1 ) }  =  { ( P ` 
0 ) ,  ( P `  1 ) } )
2928eqcoms 2432 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P `  0 )  =  ( P ` 
2 )  ->  { ( P `  2 ) ,  ( P ` 
1 ) }  =  { ( P ` 
0 ) ,  ( P `  1 ) } )
3029eqeq2d 2434 . . . . . . . . . . . . . . . . . 18  |-  ( ( P `  0 )  =  ( P ` 
2 )  ->  (
( E `  ( F `  1 )
)  =  { ( P `  2 ) ,  ( P ` 
1 ) }  <->  ( E `  ( F `  1
) )  =  {
( P `  0
) ,  ( P `
 1 ) } ) )
3127, 30syl5bb 260 . . . . . . . . . . . . . . . . 17  |-  ( ( P `  0 )  =  ( P ` 
2 )  ->  (
( E `  ( F `  1 )
)  =  { ( P `  1 ) ,  ( P ` 
2 ) }  <->  ( E `  ( F `  1
) )  =  {
( P `  0
) ,  ( P `
 1 ) } ) )
3231anbi2d 708 . . . . . . . . . . . . . . . 16  |-  ( ( P `  0 )  =  ( P ` 
2 )  ->  (
( ( E `  ( F `  0 ) )  =  { ( P `  0 ) ,  ( P ` 
1 ) }  /\  ( E `  ( F `
 1 ) )  =  { ( P `
 1 ) ,  ( P `  2
) } )  <->  ( ( E `  ( F `  0 ) )  =  { ( P `
 0 ) ,  ( P `  1
) }  /\  ( E `  ( F `  1 ) )  =  { ( P `
 0 ) ,  ( P `  1
) } ) ) )
33 eqtr3 2448 . . . . . . . . . . . . . . . . 17  |-  ( ( ( E `  ( F `  0 )
)  =  { ( P `  0 ) ,  ( P ` 
1 ) }  /\  ( E `  ( F `
 1 ) )  =  { ( P `
 0 ) ,  ( P `  1
) } )  -> 
( E `  ( F `  0 )
)  =  ( E `
 ( F ` 
1 ) ) )
34 usgraf1 24974 . . . . . . . . . . . . . . . . . . 19  |-  ( V USGrph  E  ->  E : dom  E
-1-1-> ran  E )
35 f1f 5787 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : ( 0..^ 2 ) -1-1-> dom  E  ->  F : ( 0..^ 2 ) --> dom  E )
36 2nn 10756 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  2  e.  NN
37 lbfzo0 11942 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0  e.  ( 0..^ 2 )  <->  2  e.  NN )
3836, 37mpbir 212 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  e.  ( 0..^ 2 )
39 ffvelrn 6026 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : ( 0..^ 2 ) --> dom  E  /\  0  e.  (
0..^ 2 ) )  ->  ( F ` 
0 )  e.  dom  E )
4038, 39mpan2 675 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F : ( 0..^ 2 ) --> dom  E  ->  ( F `  0 )  e.  dom  E )
41 1nn0 10874 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  e.  NN0
42 1lt2 10765 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  <  2
43 elfzo0 11943 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 1  e.  ( 0..^ 2 )  <->  ( 1  e. 
NN0  /\  2  e.  NN  /\  1  <  2
) )
4441, 36, 42, 43mpbir3an 1187 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  e.  ( 0..^ 2 )
45 ffvelrn 6026 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : ( 0..^ 2 ) --> dom  E  /\  1  e.  (
0..^ 2 ) )  ->  ( F ` 
1 )  e.  dom  E )
4644, 45mpan2 675 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F : ( 0..^ 2 ) --> dom  E  ->  ( F `  1 )  e.  dom  E )
4740, 46jca 534 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : ( 0..^ 2 ) --> dom  E  ->  ( ( F `  0
)  e.  dom  E  /\  ( F `  1
)  e.  dom  E
) )
4835, 47syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : ( 0..^ 2 ) -1-1-> dom  E  ->  (
( F `  0
)  e.  dom  E  /\  ( F `  1
)  e.  dom  E
) )
49 f1fveq 6169 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( E : dom  E -1-1-> ran 
E  /\  ( ( F `  0 )  e.  dom  E  /\  ( F `  1 )  e.  dom  E ) )  ->  ( ( E `
 ( F ` 
0 ) )  =  ( E `  ( F `  1 )
)  <->  ( F ` 
0 )  =  ( F `  1 ) ) )
5048, 49sylan2 476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( E : dom  E -1-1-> ran 
E  /\  F :
( 0..^ 2 )
-1-1-> dom  E )  -> 
( ( E `  ( F `  0 ) )  =  ( E `
 ( F ` 
1 ) )  <->  ( F `  0 )  =  ( F `  1
) ) )
51 f1fveq 6169 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F : ( 0..^ 2 ) -1-1-> dom  E  /\  ( 0  e.  ( 0..^ 2 )  /\  1  e.  ( 0..^ 2 ) ) )  ->  ( ( F `
 0 )  =  ( F `  1
)  <->  0  =  1 ) )
5238, 44, 51mpanr12 689 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : ( 0..^ 2 ) -1-1-> dom  E  ->  (
( F `  0
)  =  ( F `
 1 )  <->  0  = 
1 ) )
53 ax-1ne0 9597 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  =/=  0
54 necom 2691 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1  =/=  0  <->  0  =/=  1 )
55 df-ne 2618 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0  =/=  1  <->  -.  0  =  1 )
56 pm2.21 111 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( -.  0  =  1  -> 
( 0  =  1  ->  ( # `  F
)  =/=  2 ) )
5755, 56sylbi 198 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  =/=  1  ->  (
0  =  1  -> 
( # `  F )  =/=  2 ) )
5854, 57sylbi 198 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  =/=  0  ->  (
0  =  1  -> 
( # `  F )  =/=  2 ) )
5953, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  =  1  ->  ( # `
 F )  =/=  2 )
6052, 59syl6bi 231 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : ( 0..^ 2 ) -1-1-> dom  E  ->  (
( F `  0
)  =  ( F `
 1 )  -> 
( # `  F )  =/=  2 ) )
6160adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( E : dom  E -1-1-> ran 
E  /\  F :
( 0..^ 2 )
-1-1-> dom  E )  -> 
( ( F ` 
0 )  =  ( F `  1 )  ->  ( # `  F
)  =/=  2 ) )
6250, 61sylbid 218 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E : dom  E -1-1-> ran 
E  /\  F :
( 0..^ 2 )
-1-1-> dom  E )  -> 
( ( E `  ( F `  0 ) )  =  ( E `
 ( F ` 
1 ) )  -> 
( # `  F )  =/=  2 ) )
6362ex 435 . . . . . . . . . . . . . . . . . . 19  |-  ( E : dom  E -1-1-> ran  E  ->  ( F :
( 0..^ 2 )
-1-1-> dom  E  ->  (
( E `  ( F `  0 )
)  =  ( E `
 ( F ` 
1 ) )  -> 
( # `  F )  =/=  2 ) ) )
6434, 63syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( V USGrph  E  ->  ( F :
( 0..^ 2 )
-1-1-> dom  E  ->  (
( E `  ( F `  0 )
)  =  ( E `
 ( F ` 
1 ) )  -> 
( # `  F )  =/=  2 ) ) )
6564com13 83 . . . . . . . . . . . . . . . . 17  |-  ( ( E `  ( F `
 0 ) )  =  ( E `  ( F `  1 ) )  ->  ( F : ( 0..^ 2 ) -1-1-> dom  E  ->  ( V USGrph  E  ->  ( # `  F
)  =/=  2 ) ) )
6633, 65syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( E `  ( F `  0 )
)  =  { ( P `  0 ) ,  ( P ` 
1 ) }  /\  ( E `  ( F `
 1 ) )  =  { ( P `
 0 ) ,  ( P `  1
) } )  -> 
( F : ( 0..^ 2 ) -1-1-> dom  E  ->  ( V USGrph  E  ->  ( # `  F
)  =/=  2 ) ) )
6732, 66syl6bi 231 . . . . . . . . . . . . . . 15  |-  ( ( P `  0 )  =  ( P ` 
2 )  ->  (
( ( E `  ( F `  0 ) )  =  { ( P `  0 ) ,  ( P ` 
1 ) }  /\  ( E `  ( F `
 1 ) )  =  { ( P `
 1 ) ,  ( P `  2
) } )  -> 
( F : ( 0..^ 2 ) -1-1-> dom  E  ->  ( V USGrph  E  ->  ( # `  F
)  =/=  2 ) ) ) )
6867com3l 84 . . . . . . . . . . . . . 14  |-  ( ( ( E `  ( F `  0 )
)  =  { ( P `  0 ) ,  ( P ` 
1 ) }  /\  ( E `  ( F `
 1 ) )  =  { ( P `
 1 ) ,  ( P `  2
) } )  -> 
( F : ( 0..^ 2 ) -1-1-> dom  E  ->  ( ( P `
 0 )  =  ( P `  2
)  ->  ( V USGrph  E  ->  ( # `  F
)  =/=  2 ) ) ) )
6925, 68sylbi 198 . . . . . . . . . . . . 13  |-  ( A. k  e.  { 0 ,  1 }  ( E `  ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) }  ->  ( F : ( 0..^ 2 ) -1-1-> dom  E  ->  (
( P `  0
)  =  ( P `
 2 )  -> 
( V USGrph  E  ->  (
# `  F )  =/=  2 ) ) ) )
7024, 69sylbi 198 . . . . . . . . . . . 12  |-  ( A. k  e.  ( 0..^ 2 ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) }  ->  ( F : ( 0..^ 2 ) -1-1-> dom  E  ->  (
( P `  0
)  =  ( P `
 2 )  -> 
( V USGrph  E  ->  (
# `  F )  =/=  2 ) ) ) )
7170impcom 431 . . . . . . . . . . 11  |-  ( ( F : ( 0..^ 2 ) -1-1-> dom  E  /\  A. k  e.  ( 0..^ 2 ) ( E `  ( F `
 k ) )  =  { ( P `
 k ) ,  ( P `  (
k  +  1 ) ) } )  -> 
( ( P ` 
0 )  =  ( P `  2 )  ->  ( V USGrph  E  ->  ( # `  F
)  =/=  2 ) ) )
7271imp31 433 . . . . . . . . . 10  |-  ( ( ( ( F :
( 0..^ 2 )
-1-1-> dom  E  /\  A. k  e.  ( 0..^ 2 ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } )  /\  ( P `  0 )  =  ( P ` 
2 ) )  /\  V USGrph  E )  ->  ( # `
 F )  =/=  2 )
7322, 72syl6bi 231 . . . . . . . . 9  |-  ( (
# `  F )  =  2  ->  (
( ( ( F : ( 0..^ (
# `  F )
) -1-1-> dom  E  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } )  /\  ( P `  0 )  =  ( P `  ( # `  F ) ) )  /\  V USGrph  E )  ->  ( # `  F
)  =/=  2 ) )
74 ax-1 6 . . . . . . . . 9  |-  ( (
# `  F )  =/=  2  ->  ( ( ( ( F :
( 0..^ ( # `  F ) ) -1-1-> dom  E  /\  A. k  e.  ( 0..^ ( # `  F ) ) ( E `  ( F `
 k ) )  =  { ( P `
 k ) ,  ( P `  (
k  +  1 ) ) } )  /\  ( P `  0 )  =  ( P `  ( # `  F ) ) )  /\  V USGrph  E )  ->  ( # `  F
)  =/=  2 ) )
7573, 74pm2.61ine 2735 . . . . . . . 8  |-  ( ( ( ( F :
( 0..^ ( # `  F ) ) -1-1-> dom  E  /\  A. k  e.  ( 0..^ ( # `  F ) ) ( E `  ( F `
 k ) )  =  { ( P `
 k ) ,  ( P `  (
k  +  1 ) ) } )  /\  ( P `  0 )  =  ( P `  ( # `  F ) ) )  /\  V USGrph  E )  ->  ( # `  F
)  =/=  2 )
7675exp31 607 . . . . . . 7  |-  ( ( F : ( 0..^ ( # `  F
) ) -1-1-> dom  E  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } )  ->  (
( P `  0
)  =  ( P `
 ( # `  F
) )  ->  ( V USGrph  E  ->  ( # `  F
)  =/=  2 ) ) )
77763adant2 1024 . . . . . 6  |-  ( ( F : ( 0..^ ( # `  F
) ) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } )  ->  (
( P `  0
)  =  ( P `
 ( # `  F
) )  ->  ( V USGrph  E  ->  ( # `  F
)  =/=  2 ) ) )
7877adantld 468 . . . . 5  |-  ( ( F : ( 0..^ ( # `  F
) ) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } )  ->  (
( F ( V Paths 
E ) P  /\  ( P `  0 )  =  ( P `  ( # `  F ) ) )  ->  ( V USGrph  E  ->  ( # `  F
)  =/=  2 ) ) )
7978adantl 467 . . . 4  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  ( F : ( 0..^ ( # `  F
) ) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } ) )  -> 
( ( F ( V Paths  E ) P  /\  ( P ` 
0 )  =  ( P `  ( # `  F ) ) )  ->  ( V USGrph  E  ->  ( # `  F
)  =/=  2 ) ) )
8013, 79sylbid 218 . . 3  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  ( F : ( 0..^ ( # `  F
) ) -1-1-> dom  E  /\  P : ( 0 ... ( # `  F
) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F
) ) ( E `
 ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) } ) )  -> 
( F ( V Cycles  E ) P  -> 
( V USGrph  E  ->  (
# `  F )  =/=  2 ) ) )
8111, 80mpcom 37 . 2  |-  ( F ( V Cycles  E ) P  ->  ( V USGrph  E  ->  ( # `  F
)  =/=  2 ) )
8281impcom 431 1  |-  ( ( V USGrph  E  /\  F ( V Cycles  E ) P )  ->  ( # `  F
)  =/=  2 )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1867    =/= wne 2616   A.wral 2773   _Vcvv 3078   {cpr 3995   class class class wbr 4417   dom cdm 4845   ran crn 4846   -->wf 5588   -1-1->wf1 5589   ` cfv 5592  (class class class)co 6296   0cc0 9528   1c1 9529    + caddc 9531    < clt 9664   NNcn 10598   2c2 10648   NN0cn0 10858   ...cfz 11771  ..^cfzo 11902   #chash 12501   USGrph cusg 24944   Walks cwalk 25112   Trails ctrail 25113   Paths cpath 25114   Cycles ccycl 25121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4529  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-cnex 9584  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604  ax-pre-mulgt0 9605
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-1o 7181  df-oadd 7185  df-er 7362  df-map 7473  df-pm 7474  df-en 7569  df-dom 7570  df-sdom 7571  df-fin 7572  df-card 8363  df-cda 8587  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670  df-sub 9851  df-neg 9852  df-nn 10599  df-2 10657  df-n0 10859  df-z 10927  df-uz 11149  df-fz 11772  df-fzo 11903  df-hash 12502  df-word 12640  df-usgra 24947  df-wlk 25122  df-trail 25123  df-pth 25124  df-cycl 25127
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator