Metamath Proof Explorer

Theorem clwwlknonex2lem2

Description: Lemma 2 for clwwlknonex2 : Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018) (Revised by AV, 27-Jan-2022)

Ref Expression
Hypotheses clwwlknonex2.v 
|- V = ( Vtx ` G )
clwwlknonex2.e 
|- E = ( Edg ` G )
Assertion clwwlknonex2lem2 
|- ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> A. i e. ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( # ` W ) } ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E )

Proof

Step Hyp Ref Expression
1 clwwlknonex2.v 
 |-  V = ( Vtx ` G )
2 clwwlknonex2.e 
 |-  E = ( Edg ` G )
3 simpl 
 |-  ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) -> W e. Word V )
4 3 adantr 
 |-  ( ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> W e. Word V )
5 elfzonn0 
 |-  ( i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) -> i e. NN0 )
6 5 adantl 
 |-  ( ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> i e. NN0 )
7 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
8 elfzo0 
 |-  ( i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) <-> ( i e. NN0 /\ ( ( # ` W ) - 1 ) e. NN /\ i < ( ( # ` W ) - 1 ) ) )
9 nn0re 
 |-  ( i e. NN0 -> i e. RR )
10 9 adantr 
 |-  ( ( i e. NN0 /\ ( # ` W ) e. NN0 ) -> i e. RR )
11 nn0re 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. RR )
12 peano2rem 
 |-  ( ( # ` W ) e. RR -> ( ( # ` W ) - 1 ) e. RR )
13 11 12 syl 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - 1 ) e. RR )
14 13 adantl 
 |-  ( ( i e. NN0 /\ ( # ` W ) e. NN0 ) -> ( ( # ` W ) - 1 ) e. RR )
15 11 adantl 
 |-  ( ( i e. NN0 /\ ( # ` W ) e. NN0 ) -> ( # ` W ) e. RR )
16 10 14 15 3jca 
 |-  ( ( i e. NN0 /\ ( # ` W ) e. NN0 ) -> ( i e. RR /\ ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR ) )
17 11 ltm1d 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - 1 ) < ( # ` W ) )
18 17 adantl 
 |-  ( ( i e. NN0 /\ ( # ` W ) e. NN0 ) -> ( ( # ` W ) - 1 ) < ( # ` W ) )
19 lttr 
 |-  ( ( i e. RR /\ ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR ) -> ( ( i < ( ( # ` W ) - 1 ) /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) -> i < ( # ` W ) ) )
20 19 expcomd 
 |-  ( ( i e. RR /\ ( ( # ` W ) - 1 ) e. RR /\ ( # ` W ) e. RR ) -> ( ( ( # ` W ) - 1 ) < ( # ` W ) -> ( i < ( ( # ` W ) - 1 ) -> i < ( # ` W ) ) ) )
21 16 18 20 sylc 
 |-  ( ( i e. NN0 /\ ( # ` W ) e. NN0 ) -> ( i < ( ( # ` W ) - 1 ) -> i < ( # ` W ) ) )
22 21 impancom 
 |-  ( ( i e. NN0 /\ i < ( ( # ` W ) - 1 ) ) -> ( ( # ` W ) e. NN0 -> i < ( # ` W ) ) )
23 22 3adant2 
 |-  ( ( i e. NN0 /\ ( ( # ` W ) - 1 ) e. NN /\ i < ( ( # ` W ) - 1 ) ) -> ( ( # ` W ) e. NN0 -> i < ( # ` W ) ) )
24 8 23 sylbi 
 |-  ( i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) -> ( ( # ` W ) e. NN0 -> i < ( # ` W ) ) )
25 7 24 syl5com 
 |-  ( W e. Word V -> ( i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) -> i < ( # ` W ) ) )
26 25 adantr 
 |-  ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) -> ( i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) -> i < ( # ` W ) ) )
27 26 imp 
 |-  ( ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> i < ( # ` W ) )
28 ccat2s1fvw 
 |-  ( ( W e. Word V /\ i e. NN0 /\ i < ( # ` W ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) = ( W ` i ) )
29 4 6 27 28 syl3anc 
 |-  ( ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) = ( W ` i ) )
30 29 eqcomd 
 |-  ( ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( W ` i ) = ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) )
31 peano2nn0 
 |-  ( i e. NN0 -> ( i + 1 ) e. NN0 )
32 6 31 syl 
 |-  ( ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( i + 1 ) e. NN0 )
33 1red 
 |-  ( ( i e. NN0 /\ ( # ` W ) e. NN0 ) -> 1 e. RR )
34 10 33 15 ltaddsubd 
 |-  ( ( i e. NN0 /\ ( # ` W ) e. NN0 ) -> ( ( i + 1 ) < ( # ` W ) <-> i < ( ( # ` W ) - 1 ) ) )
35 34 biimprd 
 |-  ( ( i e. NN0 /\ ( # ` W ) e. NN0 ) -> ( i < ( ( # ` W ) - 1 ) -> ( i + 1 ) < ( # ` W ) ) )
36 35 impancom 
 |-  ( ( i e. NN0 /\ i < ( ( # ` W ) - 1 ) ) -> ( ( # ` W ) e. NN0 -> ( i + 1 ) < ( # ` W ) ) )
37 36 3adant2 
 |-  ( ( i e. NN0 /\ ( ( # ` W ) - 1 ) e. NN /\ i < ( ( # ` W ) - 1 ) ) -> ( ( # ` W ) e. NN0 -> ( i + 1 ) < ( # ` W ) ) )
38 8 37 sylbi 
 |-  ( i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) -> ( ( # ` W ) e. NN0 -> ( i + 1 ) < ( # ` W ) ) )
39 7 38 mpan9 
 |-  ( ( W e. Word V /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( i + 1 ) < ( # ` W ) )
40 39 adantlr 
 |-  ( ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( i + 1 ) < ( # ` W ) )
41 ccat2s1fvw 
 |-  ( ( W e. Word V /\ ( i + 1 ) e. NN0 /\ ( i + 1 ) < ( # ` W ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
42 4 32 40 41 syl3anc 
 |-  ( ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) = ( W ` ( i + 1 ) ) )
43 42 eqcomd 
 |-  ( ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( W ` ( i + 1 ) ) = ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) )
44 30 43 preq12d 
 |-  ( ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> { ( W ` i ) , ( W ` ( i + 1 ) ) } = { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } )
45 44 eleq1d 
 |-  ( ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) /\ i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E <-> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E ) )
46 45 ralbidva 
 |-  ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E <-> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E ) )
47 46 biimpd 
 |-  ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E ) )
48 47 impancom 
 |-  ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( ( X e. V /\ Y e. V ) -> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E ) )
49 48 3adant3 
 |-  ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( ( X e. V /\ Y e. V ) -> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E ) )
50 49 3ad2ant1 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( ( X e. V /\ Y e. V ) -> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E ) )
51 50 com12 
 |-  ( ( X e. V /\ Y e. V ) -> ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E ) )
52 51 a1dd 
 |-  ( ( X e. V /\ Y e. V ) -> ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( { X , Y } e. E -> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E ) ) )
53 52 3adant3 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( { X , Y } e. E -> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E ) ) )
54 53 imp31 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E )
55 ax-1 
 |-  ( ( X e. V /\ Y e. V ) -> ( { X , Y } e. E -> ( X e. V /\ Y e. V ) ) )
56 55 3adant3 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( { X , Y } e. E -> ( X e. V /\ Y e. V ) ) )
57 simpl 
 |-  ( ( W e. Word V /\ ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) ) -> W e. Word V )
58 oveq1 
 |-  ( ( # ` W ) = ( N - 2 ) -> ( ( # ` W ) - 1 ) = ( ( N - 2 ) - 1 ) )
59 58 adantr 
 |-  ( ( ( # ` W ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` W ) - 1 ) = ( ( N - 2 ) - 1 ) )
60 eluzelcn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. CC )
61 2cnd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. CC )
62 1cnd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. CC )
63 60 61 62 subsub4d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) - 1 ) = ( N - ( 2 + 1 ) ) )
64 2p1e3 
 |-  ( 2 + 1 ) = 3
65 64 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 2 + 1 ) = 3 )
66 65 oveq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - ( 2 + 1 ) ) = ( N - 3 ) )
67 uznn0sub 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 3 ) e. NN0 )
68 66 67 eqeltrd 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - ( 2 + 1 ) ) e. NN0 )
69 63 68 eqeltrd 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) - 1 ) e. NN0 )
70 69 adantl 
 |-  ( ( ( # ` W ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( N - 2 ) - 1 ) e. NN0 )
71 59 70 eqeltrd 
 |-  ( ( ( # ` W ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` W ) - 1 ) e. NN0 )
72 71 ancoms 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( ( # ` W ) - 1 ) e. NN0 )
73 72 adantl 
 |-  ( ( W e. Word V /\ ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) ) -> ( ( # ` W ) - 1 ) e. NN0 )
74 7 11 syl 
 |-  ( W e. Word V -> ( # ` W ) e. RR )
75 74 adantr 
 |-  ( ( W e. Word V /\ ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) ) -> ( # ` W ) e. RR )
76 75 ltm1d 
 |-  ( ( W e. Word V /\ ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) ) -> ( ( # ` W ) - 1 ) < ( # ` W ) )
77 57 73 76 3jca 
 |-  ( ( W e. Word V /\ ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) ) -> ( W e. Word V /\ ( ( # ` W ) - 1 ) e. NN0 /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) )
78 77 ex 
 |-  ( W e. Word V -> ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( W e. Word V /\ ( ( # ` W ) - 1 ) e. NN0 /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) ) )
79 78 adantr 
 |-  ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( W e. Word V /\ ( ( # ` W ) - 1 ) e. NN0 /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) ) )
80 79 3ad2ant1 
 |-  ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) -> ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( W e. Word V /\ ( ( # ` W ) - 1 ) e. NN0 /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) ) )
81 80 imp 
 |-  ( ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) /\ ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) ) -> ( W e. Word V /\ ( ( # ` W ) - 1 ) e. NN0 /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) )
82 ccat2s1fvw 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. NN0 /\ ( ( # ` W ) - 1 ) < ( # ` W ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
83 81 82 syl 
 |-  ( ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) /\ ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( # ` W ) - 1 ) ) )
84 nn0cn 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. CC )
85 ax-1cn 
 |-  1 e. CC
86 npcan 
 |-  ( ( ( # ` W ) e. CC /\ 1 e. CC ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
87 84 85 86 sylancl 
 |-  ( ( # ` W ) e. NN0 -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
88 7 87 syl 
 |-  ( W e. Word V -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
89 88 adantr 
 |-  ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
90 89 3ad2ant1 
 |-  ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
91 90 fveq2d 
 |-  ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) = ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) )
92 simp1l 
 |-  ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) -> W e. Word V )
93 eqidd 
 |-  ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) -> ( # ` W ) = ( # ` W ) )
94 simp2l 
 |-  ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) -> X e. V )
95 ccatw2s1p1 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) /\ X e. V ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) = X )
96 92 93 94 95 syl3anc 
 |-  ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) = X )
97 91 96 eqtrd 
 |-  ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) = X )
98 97 adantr 
 |-  ( ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) /\ ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) = X )
99 83 98 preq12d 
 |-  ( ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) /\ ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } = { ( W ` ( ( # ` W ) - 1 ) ) , X } )
100 lsw 
 |-  ( W e. Word V -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
101 100 adantl 
 |-  ( ( ( W ` 0 ) = X /\ W e. Word V ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
102 simpl 
 |-  ( ( ( W ` 0 ) = X /\ W e. Word V ) -> ( W ` 0 ) = X )
103 101 102 preq12d 
 |-  ( ( ( W ` 0 ) = X /\ W e. Word V ) -> { ( lastS ` W ) , ( W ` 0 ) } = { ( W ` ( ( # ` W ) - 1 ) ) , X } )
104 103 eleq1d 
 |-  ( ( ( W ` 0 ) = X /\ W e. Word V ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. E <-> { ( W ` ( ( # ` W ) - 1 ) ) , X } e. E ) )
105 104 biimpd 
 |-  ( ( ( W ` 0 ) = X /\ W e. Word V ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. E -> { ( W ` ( ( # ` W ) - 1 ) ) , X } e. E ) )
106 105 expcom 
 |-  ( W e. Word V -> ( ( W ` 0 ) = X -> ( { ( lastS ` W ) , ( W ` 0 ) } e. E -> { ( W ` ( ( # ` W ) - 1 ) ) , X } e. E ) ) )
107 106 com23 
 |-  ( W e. Word V -> ( { ( lastS ` W ) , ( W ` 0 ) } e. E -> ( ( W ` 0 ) = X -> { ( W ` ( ( # ` W ) - 1 ) ) , X } e. E ) ) )
108 107 imp31 
 |-  ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( W ` 0 ) = X ) -> { ( W ` ( ( # ` W ) - 1 ) ) , X } e. E )
109 108 3adant2 
 |-  ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) -> { ( W ` ( ( # ` W ) - 1 ) ) , X } e. E )
110 109 adantr 
 |-  ( ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) /\ ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) ) -> { ( W ` ( ( # ` W ) - 1 ) ) , X } e. E )
111 99 110 eqeltrd 
 |-  ( ( ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( X e. V /\ Y e. V ) /\ ( W ` 0 ) = X ) /\ ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E )
112 111 exp520 
 |-  ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( ( X e. V /\ Y e. V ) -> ( ( W ` 0 ) = X -> ( N e. ( ZZ>= ` 3 ) -> ( ( # ` W ) = ( N - 2 ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E ) ) ) ) )
113 112 com14 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( X e. V /\ Y e. V ) -> ( ( W ` 0 ) = X -> ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( ( # ` W ) = ( N - 2 ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E ) ) ) ) )
114 113 3ad2ant3 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( X e. V /\ Y e. V ) -> ( ( W ` 0 ) = X -> ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( ( # ` W ) = ( N - 2 ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E ) ) ) ) )
115 56 114 syld 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( { X , Y } e. E -> ( ( W ` 0 ) = X -> ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( ( # ` W ) = ( N - 2 ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E ) ) ) ) )
116 115 com25 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` W ) = ( N - 2 ) -> ( ( W ` 0 ) = X -> ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( { X , Y } e. E -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E ) ) ) ) )
117 116 com14 
 |-  ( ( W e. Word V /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( ( # ` W ) = ( N - 2 ) -> ( ( W ` 0 ) = X -> ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( { X , Y } e. E -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E ) ) ) ) )
118 117 3adant2 
 |-  ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( ( # ` W ) = ( N - 2 ) -> ( ( W ` 0 ) = X -> ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( { X , Y } e. E -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E ) ) ) ) )
119 118 3imp 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( { X , Y } e. E -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E ) ) )
120 119 impcom 
 |-  ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) -> ( { X , Y } e. E -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E ) )
121 120 imp 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E )
122 eqidd 
 |-  ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) -> ( # ` W ) = ( # ` W ) )
123 simprl 
 |-  ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) -> X e. V )
124 3 122 123 95 syl3anc 
 |-  ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) = X )
125 eqid 
 |-  ( # ` W ) = ( # ` W )
126 ccatw2s1p2 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) = Y )
127 125 126 mpanl2 
 |-  ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) = Y )
128 124 127 preq12d 
 |-  ( ( W e. Word V /\ ( X e. V /\ Y e. V ) ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } = { X , Y } )
129 128 expcom 
 |-  ( ( X e. V /\ Y e. V ) -> ( W e. Word V -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } = { X , Y } ) )
130 129 a1i 
 |-  ( { X , Y } e. E -> ( ( X e. V /\ Y e. V ) -> ( W e. Word V -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } = { X , Y } ) ) )
131 130 com13 
 |-  ( W e. Word V -> ( ( X e. V /\ Y e. V ) -> ( { X , Y } e. E -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } = { X , Y } ) ) )
132 131 3ad2ant1 
 |-  ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( ( X e. V /\ Y e. V ) -> ( { X , Y } e. E -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } = { X , Y } ) ) )
133 132 3ad2ant1 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( ( X e. V /\ Y e. V ) -> ( { X , Y } e. E -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } = { X , Y } ) ) )
134 133 com12 
 |-  ( ( X e. V /\ Y e. V ) -> ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( { X , Y } e. E -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } = { X , Y } ) ) )
135 134 3adant3 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( { X , Y } e. E -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } = { X , Y } ) ) )
136 135 imp31 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } = { X , Y } )
137 simpr 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> { X , Y } e. E )
138 136 137 eqeltrd 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } e. E )
139 ovex 
 |-  ( ( # ` W ) - 1 ) e. _V
140 fvex 
 |-  ( # ` W ) e. _V
141 fveq2 
 |-  ( i = ( ( # ` W ) - 1 ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) = ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) )
142 fvoveq1 
 |-  ( i = ( ( # ` W ) - 1 ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) = ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) )
143 141 142 preq12d 
 |-  ( i = ( ( # ` W ) - 1 ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } = { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } )
144 143 eleq1d 
 |-  ( i = ( ( # ` W ) - 1 ) -> ( { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E <-> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E ) )
145 fveq2 
 |-  ( i = ( # ` W ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) = ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) )
146 fvoveq1 
 |-  ( i = ( # ` W ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) = ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) )
147 145 146 preq12d 
 |-  ( i = ( # ` W ) -> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } = { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } )
148 147 eleq1d 
 |-  ( i = ( # ` W ) -> ( { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E <-> { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } e. E ) )
149 139 140 144 148 ralpr 
 |-  ( A. i e. { ( ( # ` W ) - 1 ) , ( # ` W ) } { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E <-> ( { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) - 1 ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( ( # ` W ) - 1 ) + 1 ) ) } e. E /\ { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( # ` W ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( # ` W ) + 1 ) ) } e. E ) )
150 121 138 149 sylanbrc 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> A. i e. { ( ( # ` W ) - 1 ) , ( # ` W ) } { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E )
151 ralunb 
 |-  ( A. i e. ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( # ` W ) } ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E <-> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E /\ A. i e. { ( ( # ` W ) - 1 ) , ( # ` W ) } { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E ) )
152 54 150 151 sylanbrc 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> A. i e. ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( # ` W ) } ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E )