Step |
Hyp |
Ref |
Expression |
1 |
|
numclwwlk.v |
|- V = ( Vtx ` G ) |
2 |
|
numclwwlk.q |
|- Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } ) |
3 |
|
numclwwlk.h |
|- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } ) |
4 |
1 2
|
numclwwlkovq |
|- ( ( X e. V /\ N e. NN ) -> ( X Q N ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) |
5 |
4
|
3adant1 |
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( X Q N ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) |
6 |
5
|
eleq2d |
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( W e. ( X Q N ) <-> W e. { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) ) |
7 |
|
fveq1 |
|- ( w = W -> ( w ` 0 ) = ( W ` 0 ) ) |
8 |
7
|
eqeq1d |
|- ( w = W -> ( ( w ` 0 ) = X <-> ( W ` 0 ) = X ) ) |
9 |
|
fveq2 |
|- ( w = W -> ( lastS ` w ) = ( lastS ` W ) ) |
10 |
9
|
neeq1d |
|- ( w = W -> ( ( lastS ` w ) =/= X <-> ( lastS ` W ) =/= X ) ) |
11 |
8 10
|
anbi12d |
|- ( w = W -> ( ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) <-> ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) |
12 |
11
|
elrab |
|- ( W e. { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } <-> ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) |
13 |
6 12
|
syl6bb |
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( W e. ( X Q N ) <-> ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) ) |
14 |
|
simpl1 |
|- ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> G e. FriendGraph ) |
15 |
|
eqid |
|- ( Edg ` G ) = ( Edg ` G ) |
16 |
1 15
|
wwlknp |
|- ( W e. ( N WWalksN G ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) |
17 |
|
peano2nn |
|- ( N e. NN -> ( N + 1 ) e. NN ) |
18 |
17
|
adantl |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ N e. NN ) -> ( N + 1 ) e. NN ) |
19 |
|
simpl |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ N e. NN ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) ) |
20 |
18 19
|
jca |
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) /\ N e. NN ) -> ( ( N + 1 ) e. NN /\ ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) ) ) |
21 |
20
|
ex |
|- ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( N e. NN -> ( ( N + 1 ) e. NN /\ ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) ) ) ) |
22 |
21
|
3adant3 |
|- ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( N e. NN -> ( ( N + 1 ) e. NN /\ ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) ) ) ) |
23 |
16 22
|
syl |
|- ( W e. ( N WWalksN G ) -> ( N e. NN -> ( ( N + 1 ) e. NN /\ ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) ) ) ) |
24 |
|
lswlgt0cl |
|- ( ( ( N + 1 ) e. NN /\ ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) ) -> ( lastS ` W ) e. V ) |
25 |
23 24
|
syl6 |
|- ( W e. ( N WWalksN G ) -> ( N e. NN -> ( lastS ` W ) e. V ) ) |
26 |
25
|
adantr |
|- ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( N e. NN -> ( lastS ` W ) e. V ) ) |
27 |
26
|
com12 |
|- ( N e. NN -> ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( lastS ` W ) e. V ) ) |
28 |
27
|
3ad2ant3 |
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( lastS ` W ) e. V ) ) |
29 |
28
|
imp |
|- ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> ( lastS ` W ) e. V ) |
30 |
|
eleq1 |
|- ( ( W ` 0 ) = X -> ( ( W ` 0 ) e. V <-> X e. V ) ) |
31 |
30
|
biimprd |
|- ( ( W ` 0 ) = X -> ( X e. V -> ( W ` 0 ) e. V ) ) |
32 |
31
|
ad2antrl |
|- ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( X e. V -> ( W ` 0 ) e. V ) ) |
33 |
32
|
com12 |
|- ( X e. V -> ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( W ` 0 ) e. V ) ) |
34 |
33
|
3ad2ant2 |
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( W ` 0 ) e. V ) ) |
35 |
34
|
imp |
|- ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> ( W ` 0 ) e. V ) |
36 |
|
neeq2 |
|- ( X = ( W ` 0 ) -> ( ( lastS ` W ) =/= X <-> ( lastS ` W ) =/= ( W ` 0 ) ) ) |
37 |
36
|
eqcoms |
|- ( ( W ` 0 ) = X -> ( ( lastS ` W ) =/= X <-> ( lastS ` W ) =/= ( W ` 0 ) ) ) |
38 |
37
|
biimpa |
|- ( ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) -> ( lastS ` W ) =/= ( W ` 0 ) ) |
39 |
38
|
adantl |
|- ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( lastS ` W ) =/= ( W ` 0 ) ) |
40 |
39
|
adantl |
|- ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> ( lastS ` W ) =/= ( W ` 0 ) ) |
41 |
29 35 40
|
3jca |
|- ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> ( ( lastS ` W ) e. V /\ ( W ` 0 ) e. V /\ ( lastS ` W ) =/= ( W ` 0 ) ) ) |
42 |
1 15
|
frcond2 |
|- ( G e. FriendGraph -> ( ( ( lastS ` W ) e. V /\ ( W ` 0 ) e. V /\ ( lastS ` W ) =/= ( W ` 0 ) ) -> E! v e. V ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) ) ) |
43 |
14 41 42
|
sylc |
|- ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> E! v e. V ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) ) |
44 |
|
simpl |
|- ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> W e. ( N WWalksN G ) ) |
45 |
44
|
ad2antlr |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> W e. ( N WWalksN G ) ) |
46 |
|
simpr |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> v e. V ) |
47 |
|
nnnn0 |
|- ( N e. NN -> N e. NN0 ) |
48 |
47
|
3ad2ant3 |
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> N e. NN0 ) |
49 |
48
|
ad2antrr |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> N e. NN0 ) |
50 |
45 46 49
|
3jca |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( W e. ( N WWalksN G ) /\ v e. V /\ N e. NN0 ) ) |
51 |
1 15
|
wwlksext2clwwlk |
|- ( ( W e. ( N WWalksN G ) /\ v e. V ) -> ( ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) ) |
52 |
51
|
3adant3 |
|- ( ( W e. ( N WWalksN G ) /\ v e. V /\ N e. NN0 ) -> ( ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) ) |
53 |
52
|
imp |
|- ( ( ( W e. ( N WWalksN G ) /\ v e. V /\ N e. NN0 ) /\ ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) ) -> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) |
54 |
50 53
|
sylan |
|- ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) ) -> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) |
55 |
1
|
wwlknbp |
|- ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) ) |
56 |
55
|
simp3d |
|- ( W e. ( N WWalksN G ) -> W e. Word V ) |
57 |
56
|
ad2antrl |
|- ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> W e. Word V ) |
58 |
57
|
ad2antrr |
|- ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> W e. Word V ) |
59 |
46
|
adantr |
|- ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> v e. V ) |
60 |
|
2z |
|- 2 e. ZZ |
61 |
|
nn0pzuz |
|- ( ( N e. NN0 /\ 2 e. ZZ ) -> ( N + 2 ) e. ( ZZ>= ` 2 ) ) |
62 |
47 60 61
|
sylancl |
|- ( N e. NN -> ( N + 2 ) e. ( ZZ>= ` 2 ) ) |
63 |
62
|
3ad2ant3 |
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( N + 2 ) e. ( ZZ>= ` 2 ) ) |
64 |
63
|
ad3antrrr |
|- ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> ( N + 2 ) e. ( ZZ>= ` 2 ) ) |
65 |
|
simpr |
|- ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) |
66 |
1 15
|
clwwlkext2edg |
|- ( ( ( W e. Word V /\ v e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) ) |
67 |
58 59 64 65 66
|
syl31anc |
|- ( ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) /\ ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) -> ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) ) |
68 |
54 67
|
impbida |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) ) ) |
69 |
46 1
|
eleqtrdi |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> v e. ( Vtx ` G ) ) |
70 |
38
|
anim2i |
|- ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( W e. ( N WWalksN G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) ) |
71 |
70
|
ad2antlr |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( W e. ( N WWalksN G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) ) |
72 |
71
|
simprd |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( lastS ` W ) =/= ( W ` 0 ) ) |
73 |
|
numclwwlk2lem1lem |
|- ( ( v e. ( Vtx ` G ) /\ W e. ( N WWalksN G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) -> ( ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) /\ ( ( W ++ <" v "> ) ` N ) =/= ( W ` 0 ) ) ) |
74 |
69 45 72 73
|
syl3anc |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) /\ ( ( W ++ <" v "> ) ` N ) =/= ( W ` 0 ) ) ) |
75 |
|
eqeq2 |
|- ( X = ( W ` 0 ) -> ( ( ( W ++ <" v "> ) ` 0 ) = X <-> ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) ) ) |
76 |
75
|
eqcoms |
|- ( ( W ` 0 ) = X -> ( ( ( W ++ <" v "> ) ` 0 ) = X <-> ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) ) ) |
77 |
76
|
ad2antrl |
|- ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> ( ( ( W ++ <" v "> ) ` 0 ) = X <-> ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) ) ) |
78 |
77
|
ad2antlr |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` 0 ) = X <-> ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) ) ) |
79 |
74
|
simpld |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) ) |
80 |
79
|
neeq2d |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` N ) =/= ( ( W ++ <" v "> ) ` 0 ) <-> ( ( W ++ <" v "> ) ` N ) =/= ( W ` 0 ) ) ) |
81 |
78 80
|
anbi12d |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` N ) =/= ( ( W ++ <" v "> ) ` 0 ) ) <-> ( ( ( W ++ <" v "> ) ` 0 ) = ( W ` 0 ) /\ ( ( W ++ <" v "> ) ` N ) =/= ( W ` 0 ) ) ) ) |
82 |
74 81
|
mpbird |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` N ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) |
83 |
|
nncn |
|- ( N e. NN -> N e. CC ) |
84 |
|
2cnd |
|- ( N e. NN -> 2 e. CC ) |
85 |
83 84
|
pncand |
|- ( N e. NN -> ( ( N + 2 ) - 2 ) = N ) |
86 |
85
|
3ad2ant3 |
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( N + 2 ) - 2 ) = N ) |
87 |
86
|
ad2antrr |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( N + 2 ) - 2 ) = N ) |
88 |
87
|
fveq2d |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) = ( ( W ++ <" v "> ) ` N ) ) |
89 |
88
|
neeq1d |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) <-> ( ( W ++ <" v "> ) ` N ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) |
90 |
89
|
anbi2d |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) <-> ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` N ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) ) |
91 |
82 90
|
mpbird |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) |
92 |
91
|
biantrud |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) <-> ( ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) ) ) |
93 |
62
|
anim2i |
|- ( ( X e. V /\ N e. NN ) -> ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) ) |
94 |
93
|
3adant1 |
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) ) |
95 |
94
|
ad2antrr |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) ) |
96 |
3
|
numclwwlkovh |
|- ( ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) -> ( X H ( N + 2 ) ) = { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } ) |
97 |
95 96
|
syl |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( X H ( N + 2 ) ) = { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } ) |
98 |
97
|
eleq2d |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) <-> ( W ++ <" v "> ) e. { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } ) ) |
99 |
|
fveq1 |
|- ( w = ( W ++ <" v "> ) -> ( w ` 0 ) = ( ( W ++ <" v "> ) ` 0 ) ) |
100 |
99
|
eqeq1d |
|- ( w = ( W ++ <" v "> ) -> ( ( w ` 0 ) = X <-> ( ( W ++ <" v "> ) ` 0 ) = X ) ) |
101 |
|
fveq1 |
|- ( w = ( W ++ <" v "> ) -> ( w ` ( ( N + 2 ) - 2 ) ) = ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) ) |
102 |
101 99
|
neeq12d |
|- ( w = ( W ++ <" v "> ) -> ( ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) <-> ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) |
103 |
100 102
|
anbi12d |
|- ( w = ( W ++ <" v "> ) -> ( ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) <-> ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) ) |
104 |
103
|
elrab |
|- ( ( W ++ <" v "> ) e. { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } <-> ( ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) ) |
105 |
98 104
|
bitr2di |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( ( W ++ <" v "> ) e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( ( W ++ <" v "> ) ` 0 ) = X /\ ( ( W ++ <" v "> ) ` ( ( N + 2 ) - 2 ) ) =/= ( ( W ++ <" v "> ) ` 0 ) ) ) <-> ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) ) |
106 |
68 92 105
|
3bitrd |
|- ( ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) /\ v e. V ) -> ( ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) <-> ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) ) |
107 |
106
|
reubidva |
|- ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> ( E! v e. V ( { ( lastS ` W ) , v } e. ( Edg ` G ) /\ { v , ( W ` 0 ) } e. ( Edg ` G ) ) <-> E! v e. V ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) ) |
108 |
43 107
|
mpbid |
|- ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) ) -> E! v e. V ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) |
109 |
108
|
ex |
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( W e. ( N WWalksN G ) /\ ( ( W ` 0 ) = X /\ ( lastS ` W ) =/= X ) ) -> E! v e. V ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) ) |
110 |
13 109
|
sylbid |
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( W e. ( X Q N ) -> E! v e. V ( W ++ <" v "> ) e. ( X H ( N + 2 ) ) ) ) |