Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  numclwlk1lem2foa Structured version   Unicode version
Theorem numclwlk1lem2foa 30833
Description: Going forth and back form the end of a (closed) walk. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
Hypotheses
Ref Expression
numclwwlk.c |- C = ( n e. NN0 |-> ( ( V ClWWalksN E ) ` n ) )
numclwwlk.f |- F = ( v e. V , n e. NN0 |-> { w e. ( C ` n ) | ( w ` 0 ) = v } )
numclwwlk.g |- G = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( C ` n ) | ( ( w ` 0 ) = v /\ ( w ` ( n - 2 ) ) = ( w ` 0 ) ) } )
Assertion
Ref Expression
numclwlk1lem2foa |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( P e. ( X F ( N - 2 ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( P concat <" X "> ) concat <" Q "> ) e. ( X G N ) ) )
Distinct variable groups:   n, E   n, N   n, V   w, C   w, N   C, n, v, w   v, N   n, X, v, w   v, V   w, E   w, V   w, F   w, P   w, Q
Allowed substitution hints:   P( v, n)   Q( v, n)   E( v)   F( v, n)   G( w, v, n)
Proof of Theorem numclwlk1lem2foa
Dummy variable i is distinct from all other variables.
StepHypRef Expression
1 simp1 988 . . . . . . . . . 10 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> V USGrph E )
2 uzuzle23 30342 . . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
3 uznn0sub 11004 . . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. NN0 )
42, 3syl 16 . . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN0 )
543ad2ant3 1011 . . . . . . . . . 10 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 2 ) e. NN0 )
6 simp2 989 . . . . . . . . . 10 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> X e. V )
7 numclwwlk.c . . . . . . . . . . 11 |- C = ( n e. NN0 |-> ( ( V ClWWalksN E ) ` n ) )
8 numclwwlk.f . . . . . . . . . . 11 |- F = ( v e. V , n e. NN0 |-> { w e. ( C ` n ) | ( w ` 0 ) = v } )
97, 8numclwwlkovfel2 30825 . . . . . . . . . 10 |- ( ( V USGrph E /\ ( N - 2 ) e. NN0 /\ X e. V ) -> ( P e. ( X F ( N - 2 ) ) <-> ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) )
101, 5, 6, 9syl3anc 1219 . . . . . . . . 9 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( P e. ( X F ( N - 2 ) ) <-> ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) )
11 simplll 757 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) /\ P e. ( X F ( N - 2 ) ) ) -> ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) )
12 simpr 461 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> Q e. ( <. V , E >. Neighbors X ) )
1312adantr 465 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) /\ P e. ( X F ( N - 2 ) ) ) -> Q e. ( <. V , E >. Neighbors X ) )
14 simpr 461 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) /\ P e. ( X F ( N - 2 ) ) ) -> P e. ( X F ( N - 2 ) ) )
157, 8numclwwlkovf2ex 30828 . . . . . . . . . . . . . . . . 17 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ Q e. ( <. V , E >. Neighbors X ) /\ P e. ( X F ( N - 2 ) ) ) -> ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) )
1611, 13, 14, 15syl3anc 1219 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) /\ P e. ( X F ( N - 2 ) ) ) -> ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) )
17 nbgraisvtx 23495 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( V USGrph E -> ( Q e. ( <. V , E >. Neighbors X ) -> Q e. V ) )
18173ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> Q e. V ) )
1918adantr 465 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> Q e. V ) )
20 simplll 757 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Q e. V ) -> P e. Word V )
21 s1cl 12412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( X e. V -> <" X "> e. Word V )
22213ad2ant2 1010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> <" X "> e. Word V )
2322adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> <" X "> e. Word V )
2423adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Q e. V ) -> <" X "> e. Word V )
25 s1cl 12412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( Q e. V -> <" Q "> e. Word V )
2625adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Q e. V ) -> <" Q "> e. Word V )
27 ccatass 12405 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( P e. Word V /\ <" X "> e. Word V /\ <" Q "> e. Word V ) -> ( ( P concat <" X "> ) concat <" Q "> ) = ( P concat ( <" X "> concat <" Q "> ) ) )
2827oveq1d 6216 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( P e. Word V /\ <" X "> e. Word V /\ <" Q "> e. Word V ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) = ( ( P concat ( <" X "> concat <" Q "> ) ) substr <. 0 , ( N - 2 ) >. ) )
2920, 24, 26, 28syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Q e. V ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) = ( ( P concat ( <" X "> concat <" Q "> ) ) substr <. 0 , ( N - 2 ) >. ) )
30 ccatcl 12393 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( <" X "> e. Word V /\ <" Q "> e. Word V ) -> ( <" X "> concat <" Q "> ) e. Word V )
3123, 25, 30syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Q e. V ) -> ( <" X "> concat <" Q "> ) e. Word V )
32 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) -> ( # ` P ) = ( N - 2 ) )
3332eqcomd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) -> ( N - 2 ) = ( # ` P ) )
3433adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( N - 2 ) = ( # ` P ) )
3534adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Q e. V ) -> ( N - 2 ) = ( # ` P ) )
36 swrdccatid 12507 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( P e. Word V /\ ( <" X "> concat <" Q "> ) e. Word V /\ ( N - 2 ) = ( # ` P ) ) -> ( ( P concat ( <" X "> concat <" Q "> ) ) substr <. 0 , ( N - 2 ) >. ) = P )
3720, 31, 35, 36syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Q e. V ) -> ( ( P concat ( <" X "> concat <" Q "> ) ) substr <. 0 , ( N - 2 ) >. ) = P )
3829, 37eqtr2d 2496 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ Q e. V ) -> P = ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) )
3938exp31 604 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. V -> P = ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) ) ) )
4039adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. V -> P = ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) ) ) )
4140impcom 430 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> ( Q e. V -> P = ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) ) )
4219, 41syld 44 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> P = ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) ) )
4342imp 429 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> P = ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) )
4443eleq1d 2523 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( P e. ( X F ( N - 2 ) ) <-> ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) ) )
4544biimpd 207 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( P e. ( X F ( N - 2 ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) ) )
4645imp 429 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) /\ P e. ( X F ( N - 2 ) ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) )
47 simplrl 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. V ) -> ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) )
486adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> X e. V )
4948anim1i 568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. V ) -> ( X e. V /\ Q e. V ) )
5047, 49jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. V ) -> ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( X e. V /\ Q e. V ) ) )
51 ccatw2s1p2 30419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( N - 2 ) + 1 ) ) = Q )
5250, 51syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. V ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( N - 2 ) + 1 ) ) = Q )
53 eluzelcn 10984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. ( ZZ>= ` 3 ) -> N e. CC )
54 2cnd 10506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. ( ZZ>= ` 3 ) -> 2 e. CC )
55 ax-1cn 9452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- 1 e. CC
5655a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. ( ZZ>= ` 3 ) -> 1 e. CC )
57 subsub 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( N e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( N - ( 2 - 1 ) ) = ( ( N - 2 ) + 1 ) )
5857eqcomd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( N e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( N - 2 ) + 1 ) = ( N - ( 2 - 1 ) ) )
5953, 54, 56, 58syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) + 1 ) = ( N - ( 2 - 1 ) ) )
60 2m1e1 10548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 2 - 1 ) = 1
6160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. ( ZZ>= ` 3 ) -> ( 2 - 1 ) = 1 )
6261oveq2d 6217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. ( ZZ>= ` 3 ) -> ( N - ( 2 - 1 ) ) = ( N - 1 ) )
6359, 62eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) + 1 ) = ( N - 1 ) )
64633ad2ant3 1011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( N - 2 ) + 1 ) = ( N - 1 ) )
6564adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> ( ( N - 2 ) + 1 ) = ( N - 1 ) )
6665adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. V ) -> ( ( N - 2 ) + 1 ) = ( N - 1 ) )
6766fveq2d 5804 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. V ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( N - 2 ) + 1 ) ) = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) )
6852, 67eqtr3d 2497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. V ) -> Q = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) )
6968ex 434 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> ( Q e. V -> Q = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) ) )
7019, 69syld 44 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> Q = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) ) )
7170impcom 430 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) ) -> Q = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) )
7271eleq1d 2523 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) ) -> ( Q e. ( <. V , E >. Neighbors X ) <-> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) ) )
7372biimpd 207 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) ) )
7473ex 434 . . . . . . . . . . . . . . . . . . . 20 |- ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) ) ) )
7574pm2.43a 49 . . . . . . . . . . . . . . . . . . 19 |- ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) ) )
7675impcom 430 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) )
7776adantr 465 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) /\ P e. ( X F ( N - 2 ) ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) )
78 ccatw2s1p1 30418 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X )
7950, 78syl 16 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. V ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X )
8079ex 434 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> ( Q e. V -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) )
8119, 80syld 44 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) )
8281imp 429 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X )
8382adantr 465 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) /\ P e. ( X F ( N - 2 ) ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X )
8446, 77, 833jca 1168 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) /\ P e. ( X F ( N - 2 ) ) ) -> ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) )
8516, 84jca 532 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) /\ P e. ( X F ( N - 2 ) ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) )
8685exp31 604 . . . . . . . . . . . . . 14 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( P e. ( X F ( N - 2 ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) ) ) )
8786expcom 435 . . . . . . . . . . . . 13 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( P e. ( X F ( N - 2 ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) ) ) ) )
8887exp31 604 . . . . . . . . . . . 12 |- ( P e. Word V -> ( ( # ` P ) = ( N - 2 ) -> ( ( P ` 0 ) = X -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( P e. ( X F ( N - 2 ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) ) ) ) ) ) )
89883ad2ant1 1009 . . . . . . . . . . 11 |- ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( # ` P ) = ( N - 2 ) -> ( ( P ` 0 ) = X -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( P e. ( X F ( N - 2 ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) ) ) ) ) ) )
90893imp 1182 . . . . . . . . . 10 |- ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( P e. ( X F ( N - 2 ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) ) ) ) )
9190com12 31 . . . . . . . . 9 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( P e. ( X F ( N - 2 ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) ) ) ) )
9210, 91sylbid 215 . . . . . . . 8 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( P e. ( X F ( N - 2 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( P e. ( X F ( N - 2 ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) ) ) ) )
9392com14 88 . . . . . . 7 |- ( P e. ( X F ( N - 2 ) ) -> ( P e. ( X F ( N - 2 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) ) ) ) )
9493pm2.43i 47 . . . . . 6 |- ( P e. ( X F ( N - 2 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) ) ) )
9594imp 429 . . . . 5 |- ( ( P e. ( X F ( N - 2 ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) ) )
9695impcom 430 . . . 4 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( P e. ( X F ( N - 2 ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) )
97 oveq1 6208 . . . . . . 7 |- ( w = ( ( P concat <" X "> ) concat <" Q "> ) -> ( w substr <. 0 , ( N - 2 ) >. ) = ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) )
9897eleq1d 2523 . . . . . 6 |- ( w = ( ( P concat <" X "> ) concat <" Q "> ) -> ( ( w substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) <-> ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) ) )
99 fveq1 5799 . . . . . . 7 |- ( w = ( ( P concat <" X "> ) concat <" Q "> ) -> ( w ` ( N - 1 ) ) = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) )
10099eleq1d 2523 . . . . . 6 |- ( w = ( ( P concat <" X "> ) concat <" Q "> ) -> ( ( w ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) <-> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) ) )
101 fveq1 5799 . . . . . . 7 |- ( w = ( ( P concat <" X "> ) concat <" Q "> ) -> ( w ` ( N - 2 ) ) = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) )
102101eqeq1d 2456 . . . . . 6 |- ( w = ( ( P concat <" X "> ) concat <" Q "> ) -> ( ( w ` ( N - 2 ) ) = X <-> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) )
10398, 100, 1023anbi123d 1290 . . . . 5 |- ( w = ( ( P concat <" X "> ) concat <" Q "> ) -> ( ( ( w substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( w ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( w ` ( N - 2 ) ) = X ) <-> ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) )
104103elrab 3224 . . . 4 |- ( ( ( P concat <" X "> ) concat <" Q "> ) e. { w e. ( C ` N ) | ( ( w substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( w ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( w ` ( N - 2 ) ) = X ) } <-> ( ( ( P concat <" X "> ) concat <" Q "> ) e. ( C ` N ) /\ ( ( ( ( P concat <" X "> ) concat <" Q "> ) substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( N - 2 ) ) = X ) ) )
10596, 104sylibr 212 . . 3 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( P e. ( X F ( N - 2 ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) ) -> ( ( P concat <" X "> ) concat <" Q "> ) e. { w e. ( C ` N ) | ( ( w substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( w ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( w ` ( N - 2 ) ) = X ) } )
106 numclwwlk.g . . . . 5 |- G = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( C ` n ) | ( ( w ` 0 ) = v /\ ( w ` ( n - 2 ) ) = ( w ` 0 ) ) } )
1077, 8, 106extwwlkfab 30832 . . . 4 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X G N ) = { w e. ( C ` N ) | ( ( w substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( w ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( w ` ( N - 2 ) ) = X ) } )
108107adantr 465 . . 3 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( P e. ( X F ( N - 2 ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) ) -> ( X G N ) = { w e. ( C ` N ) | ( ( w substr <. 0 , ( N - 2 ) >. ) e. ( X F ( N - 2 ) ) /\ ( w ` ( N - 1 ) ) e. ( <. V , E >. Neighbors X ) /\ ( w ` ( N - 2 ) ) = X ) } )
109105, 108eleqtrrd 2545 . 2 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( P e. ( X F ( N - 2 ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) ) -> ( ( P concat <" X "> ) concat <" Q "> ) e. ( X G N ) )
110109ex 434 1 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( P e. ( X F ( N - 2 ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( P concat <" X "> ) concat <" Q "> ) e. ( X G N ) ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   A.wral 2799   {crab 2803   {cpr 3988   <.cop 3992   class class class wbr 4401   |-> cmpt 4459   ran crn 4950   ` cfv 5527  (class class class)co 6201   |-> cmpt2 6203   CCcc 9392   0cc0 9394   1c1 9395   + caddc 9397   - cmin 9707   2c2 10483   3c3 10484   NN0cn0 10691   ZZ>=cuz 10973  ..^cfzo 11666   #chash 12221  Word cword 12340   lastS clsw 12341   concat cconcat 12342   <"cs1 12343   substr csubstr 12344   USGrph cusg 23417   Neighbors cnbgra 23482   ClWWalksN cclwwlkn 30563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4512  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-cnex 9450  ax-resscn 9451  ax-1cn 9452  ax-icn 9453  ax-addcl 9454  ax-addrcl 9455  ax-mulcl 9456  ax-mulrcl 9457  ax-mulcom 9458  ax-addass 9459  ax-mulass 9460  ax-distr 9461  ax-i2m1 9462  ax-1ne0 9463  ax-1rid 9464  ax-rnegex 9465  ax-rrecex 9466  ax-cnre 9467  ax-pre-lttri 9468  ax-pre-lttrn 9469  ax-pre-ltadd 9470  ax-pre-mulgt0 9471
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-tp 3991  df-op 3993  df-uni 4201  df-int 4238  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-tr 4495  df-eprel 4741  df-id 4745  df-po 4750  df-so 4751  df-fr 4788  df-we 4790  df-ord 4831  df-on 4832  df-lim 4833  df-suc 4834  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-riota 6162  df-ov 6204  df-oprab 6205  df-mpt2 6206  df-om 6588  df-1st 6688  df-2nd 6689  df-recs 6943  df-rdg 6977  df-1o 7031  df-oadd 7035  df-er 7212  df-map 7327  df-pm 7328  df-en 7422  df-dom 7423  df-sdom 7424  df-fin 7425  df-card 8221  df-pnf 9532  df-mnf 9533  df-xr 9534  df-ltxr 9535  df-le 9536  df-sub 9709  df-neg 9710  df-nn 10435  df-2 10492  df-3 10493  df-n0 10692  df-z 10759  df-uz 10974  df-fz 11556  df-fzo 11667  df-hash 12222  df-word 12348  df-lsw 12349  df-concat 12350  df-s1 12351  df-substr 12352  df-s2 12594  df-usgra 23419  df-nbgra 23485  df-clwwlk 30565  df-clwwlkn 30566
This theorem is referenced by:  numclwlk1lem2fo  30837
  Copyright terms: Public domain W3C validator