Metamath Proof Explorer

Theorem wlkp1lem8

Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)

Ref Expression
Hypotheses wlkp1.v 
|- V = ( Vtx ` G )
wlkp1.i 
|- I = ( iEdg ` G )
wlkp1.f 
|- ( ph -> Fun I )
wlkp1.a 
|- ( ph -> I e. Fin )
wlkp1.b 
|- ( ph -> B e. W )
wlkp1.c 
|- ( ph -> C e. V )
wlkp1.d 
|- ( ph -> -. B e. dom I )
wlkp1.w 
|- ( ph -> F ( Walks ` G ) P )
wlkp1.n 
|- N = ( # ` F )
wlkp1.e 
|- ( ph -> E e. ( Edg ` G ) )
wlkp1.x 
|- ( ph -> { ( P ` N ) , C } C_ E )
wlkp1.u 
|- ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
wlkp1.h 
|- H = ( F u. { <. N , B >. } )
wlkp1.q 
|- Q = ( P u. { <. ( N + 1 ) , C >. } )
wlkp1.s 
|- ( ph -> ( Vtx ` S ) = V )
wlkp1.l 
|- ( ( ph /\ C = ( P ` N ) ) -> E = { C } )
Assertion wlkp1lem8 
|- ( ph -> A. k e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 wlkp1.v 
 |-  V = ( Vtx ` G )
2 wlkp1.i 
 |-  I = ( iEdg ` G )
3 wlkp1.f 
 |-  ( ph -> Fun I )
4 wlkp1.a 
 |-  ( ph -> I e. Fin )
5 wlkp1.b 
 |-  ( ph -> B e. W )
6 wlkp1.c 
 |-  ( ph -> C e. V )
7 wlkp1.d 
 |-  ( ph -> -. B e. dom I )
8 wlkp1.w 
 |-  ( ph -> F ( Walks ` G ) P )
9 wlkp1.n 
 |-  N = ( # ` F )
10 wlkp1.e 
 |-  ( ph -> E e. ( Edg ` G ) )
11 wlkp1.x 
 |-  ( ph -> { ( P ` N ) , C } C_ E )
12 wlkp1.u 
 |-  ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
13 wlkp1.h 
 |-  H = ( F u. { <. N , B >. } )
14 wlkp1.q 
 |-  Q = ( P u. { <. ( N + 1 ) , C >. } )
15 wlkp1.s 
 |-  ( ph -> ( Vtx ` S ) = V )
16 wlkp1.l 
 |-  ( ( ph /\ C = ( P ` N ) ) -> E = { C } )
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem6 
 |-  ( ph -> A. k e. ( 0 ..^ N ) ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) )
18 10 elfvexd 
 |-  ( ph -> G e. _V )
19 1 2 iswlkg 
 |-  ( G e. _V -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
20 18 19 syl 
 |-  ( ph -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
21 9 eqcomi 
 |-  ( # ` F ) = N
22 21 oveq2i 
 |-  ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N )
23 22 raleqi 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> A. k e. ( 0 ..^ N ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
24 23 biimpi 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ N ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
25 24 3ad2ant3 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> A. k e. ( 0 ..^ N ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
26 20 25 syl6bi 
 |-  ( ph -> ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ N ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
27 8 26 mpd 
 |-  ( ph -> A. k e. ( 0 ..^ N ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
28 eqeq12 
 |-  ( ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) ) -> ( ( Q ` k ) = ( Q ` ( k + 1 ) ) <-> ( P ` k ) = ( P ` ( k + 1 ) ) ) )
29 28 3adant3 
 |-  ( ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) -> ( ( Q ` k ) = ( Q ` ( k + 1 ) ) <-> ( P ` k ) = ( P ` ( k + 1 ) ) ) )
30 simp3 
 |-  ( ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) -> ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) )
31 simp1 
 |-  ( ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) -> ( Q ` k ) = ( P ` k ) )
32 31 sneqd 
 |-  ( ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) -> { ( Q ` k ) } = { ( P ` k ) } )
33 30 32 eqeq12d 
 |-  ( ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) -> ( ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } <-> ( I ` ( F ` k ) ) = { ( P ` k ) } ) )
34 preq12 
 |-  ( ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) ) -> { ( Q ` k ) , ( Q ` ( k + 1 ) ) } = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
35 34 3adant3 
 |-  ( ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) -> { ( Q ` k ) , ( Q ` ( k + 1 ) ) } = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
36 35 30 sseq12d 
 |-  ( ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) -> ( { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) <-> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
37 29 33 36 ifpbi123d 
 |-  ( ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) -> ( if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) <-> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
38 37 biimprd 
 |-  ( ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) ) )
39 38 ral2imi 
 |-  ( A. k e. ( 0 ..^ N ) ( ( Q ` k ) = ( P ` k ) /\ ( Q ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) /\ ( ( iEdg ` S ) ` ( H ` k ) ) = ( I ` ( F ` k ) ) ) -> ( A. k e. ( 0 ..^ N ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ N ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) ) )
40 17 27 39 sylc 
 |-  ( ph -> A. k e. ( 0 ..^ N ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) )
41 1 2 3 4 5 6 7 8 9 10 11 12 13 wlkp1lem3 
 |-  ( ph -> ( ( iEdg ` S ) ` ( H ` N ) ) = ( ( I u. { <. B , E >. } ) ` B ) )
42 41 adantr 
 |-  ( ( ph /\ ( Q ` N ) = ( Q ` ( N + 1 ) ) ) -> ( ( iEdg ` S ) ` ( H ` N ) ) = ( ( I u. { <. B , E >. } ) ` B ) )
43 5 10 7 3jca 
 |-  ( ph -> ( B e. W /\ E e. ( Edg ` G ) /\ -. B e. dom I ) )
44 43 adantr 
 |-  ( ( ph /\ ( Q ` N ) = ( Q ` ( N + 1 ) ) ) -> ( B e. W /\ E e. ( Edg ` G ) /\ -. B e. dom I ) )
45 fsnunfv 
 |-  ( ( B e. W /\ E e. ( Edg ` G ) /\ -. B e. dom I ) -> ( ( I u. { <. B , E >. } ) ` B ) = E )
46 44 45 syl 
 |-  ( ( ph /\ ( Q ` N ) = ( Q ` ( N + 1 ) ) ) -> ( ( I u. { <. B , E >. } ) ` B ) = E )
47 fveq2 
 |-  ( x = N -> ( Q ` x ) = ( Q ` N ) )
48 fveq2 
 |-  ( x = N -> ( P ` x ) = ( P ` N ) )
49 47 48 eqeq12d 
 |-  ( x = N -> ( ( Q ` x ) = ( P ` x ) <-> ( Q ` N ) = ( P ` N ) ) )
50 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem5 
 |-  ( ph -> A. x e. ( 0 ... N ) ( Q ` x ) = ( P ` x ) )
51 2 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
52 lencl 
 |-  ( F e. Word dom I -> ( # ` F ) e. NN0 )
53 9 eleq1i 
 |-  ( N e. NN0 <-> ( # ` F ) e. NN0 )
54 elnn0uz 
 |-  ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
55 53 54 sylbb1 
 |-  ( ( # ` F ) e. NN0 -> N e. ( ZZ>= ` 0 ) )
56 52 55 syl 
 |-  ( F e. Word dom I -> N e. ( ZZ>= ` 0 ) )
57 8 51 56 3syl 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
58 57 54 sylibr 
 |-  ( ph -> N e. NN0 )
59 nn0fz0 
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
60 58 59 sylib 
 |-  ( ph -> N e. ( 0 ... N ) )
61 49 50 60 rspcdva 
 |-  ( ph -> ( Q ` N ) = ( P ` N ) )
62 14 fveq1i 
 |-  ( Q ` ( N + 1 ) ) = ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) )
63 ovex 
 |-  ( N + 1 ) e. _V
64 1 2 3 4 5 6 7 8 9 wlkp1lem1 
 |-  ( ph -> -. ( N + 1 ) e. dom P )
65 fsnunfv 
 |-  ( ( ( N + 1 ) e. _V /\ C e. V /\ -. ( N + 1 ) e. dom P ) -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) = C )
66 63 6 64 65 mp3an2i 
 |-  ( ph -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) = C )
67 62 66 syl5eq 
 |-  ( ph -> ( Q ` ( N + 1 ) ) = C )
68 67 eqeq2d 
 |-  ( ph -> ( ( P ` N ) = ( Q ` ( N + 1 ) ) <-> ( P ` N ) = C ) )
69 eqcom 
 |-  ( ( P ` N ) = C <-> C = ( P ` N ) )
70 68 69 bitrdi 
 |-  ( ph -> ( ( P ` N ) = ( Q ` ( N + 1 ) ) <-> C = ( P ` N ) ) )
71 sneq 
 |-  ( C = ( P ` N ) -> { C } = { ( P ` N ) } )
72 71 adantl 
 |-  ( ( ph /\ C = ( P ` N ) ) -> { C } = { ( P ` N ) } )
73 16 72 eqtrd 
 |-  ( ( ph /\ C = ( P ` N ) ) -> E = { ( P ` N ) } )
74 73 ex 
 |-  ( ph -> ( C = ( P ` N ) -> E = { ( P ` N ) } ) )
75 70 74 sylbid 
 |-  ( ph -> ( ( P ` N ) = ( Q ` ( N + 1 ) ) -> E = { ( P ` N ) } ) )
76 eqeq1 
 |-  ( ( Q ` N ) = ( P ` N ) -> ( ( Q ` N ) = ( Q ` ( N + 1 ) ) <-> ( P ` N ) = ( Q ` ( N + 1 ) ) ) )
77 sneq 
 |-  ( ( Q ` N ) = ( P ` N ) -> { ( Q ` N ) } = { ( P ` N ) } )
78 77 eqeq2d 
 |-  ( ( Q ` N ) = ( P ` N ) -> ( E = { ( Q ` N ) } <-> E = { ( P ` N ) } ) )
79 76 78 imbi12d 
 |-  ( ( Q ` N ) = ( P ` N ) -> ( ( ( Q ` N ) = ( Q ` ( N + 1 ) ) -> E = { ( Q ` N ) } ) <-> ( ( P ` N ) = ( Q ` ( N + 1 ) ) -> E = { ( P ` N ) } ) ) )
80 75 79 syl5ibrcom 
 |-  ( ph -> ( ( Q ` N ) = ( P ` N ) -> ( ( Q ` N ) = ( Q ` ( N + 1 ) ) -> E = { ( Q ` N ) } ) ) )
81 61 80 mpd 
 |-  ( ph -> ( ( Q ` N ) = ( Q ` ( N + 1 ) ) -> E = { ( Q ` N ) } ) )
82 81 imp 
 |-  ( ( ph /\ ( Q ` N ) = ( Q ` ( N + 1 ) ) ) -> E = { ( Q ` N ) } )
83 42 46 82 3eqtrd 
 |-  ( ( ph /\ ( Q ` N ) = ( Q ` ( N + 1 ) ) ) -> ( ( iEdg ` S ) ` ( H ` N ) ) = { ( Q ` N ) } )
84 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem7 
 |-  ( ph -> { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` N ) ) )
85 84 adantr 
 |-  ( ( ph /\ -. ( Q ` N ) = ( Q ` ( N + 1 ) ) ) -> { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` N ) ) )
86 83 85 ifpimpda 
 |-  ( ph -> if- ( ( Q ` N ) = ( Q ` ( N + 1 ) ) , ( ( iEdg ` S ) ` ( H ` N ) ) = { ( Q ` N ) } , { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` N ) ) ) )
87 1 2 3 4 5 6 7 8 9 10 11 12 13 wlkp1lem2 
 |-  ( ph -> ( # ` H ) = ( N + 1 ) )
88 87 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` H ) ) = ( 0 ..^ ( N + 1 ) ) )
89 fzosplitsn 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) )
90 57 89 syl 
 |-  ( ph -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) )
91 88 90 eqtrd 
 |-  ( ph -> ( 0 ..^ ( # ` H ) ) = ( ( 0 ..^ N ) u. { N } ) )
92 91 raleqdv 
 |-  ( ph -> ( A. k e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) <-> A. k e. ( ( 0 ..^ N ) u. { N } ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) ) )
93 ralunb 
 |-  ( A. k e. ( ( 0 ..^ N ) u. { N } ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) <-> ( A. k e. ( 0 ..^ N ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) /\ A. k e. { N } if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) ) )
94 93 a1i 
 |-  ( ph -> ( A. k e. ( ( 0 ..^ N ) u. { N } ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) <-> ( A. k e. ( 0 ..^ N ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) /\ A. k e. { N } if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) ) ) )
95 9 fvexi 
 |-  N e. _V
96 wkslem1 
 |-  ( k = N -> ( if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) <-> if- ( ( Q ` N ) = ( Q ` ( N + 1 ) ) , ( ( iEdg ` S ) ` ( H ` N ) ) = { ( Q ` N ) } , { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` N ) ) ) ) )
97 96 ralsng 
 |-  ( N e. _V -> ( A. k e. { N } if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) <-> if- ( ( Q ` N ) = ( Q ` ( N + 1 ) ) , ( ( iEdg ` S ) ` ( H ` N ) ) = { ( Q ` N ) } , { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` N ) ) ) ) )
98 95 97 mp1i 
 |-  ( ph -> ( A. k e. { N } if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) <-> if- ( ( Q ` N ) = ( Q ` ( N + 1 ) ) , ( ( iEdg ` S ) ` ( H ` N ) ) = { ( Q ` N ) } , { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` N ) ) ) ) )
99 98 anbi2d 
 |-  ( ph -> ( ( A. k e. ( 0 ..^ N ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) /\ A. k e. { N } if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) ) <-> ( A. k e. ( 0 ..^ N ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) /\ if- ( ( Q ` N ) = ( Q ` ( N + 1 ) ) , ( ( iEdg ` S ) ` ( H ` N ) ) = { ( Q ` N ) } , { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` N ) ) ) ) ) )
100 92 94 99 3bitrd 
 |-  ( ph -> ( A. k e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) <-> ( A. k e. ( 0 ..^ N ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) /\ if- ( ( Q ` N ) = ( Q ` ( N + 1 ) ) , ( ( iEdg ` S ) ` ( H ` N ) ) = { ( Q ` N ) } , { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` N ) ) ) ) ) )
101 40 86 100 mpbir2and 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` k ) = ( Q ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( H ` k ) ) = { ( Q ` k ) } , { ( Q ` k ) , ( Q ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` k ) ) ) )