This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlkp1lem5

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 )
Assertion wlkp1lem5 
|- ( ph -> A. k e. ( 0 ... N ) ( Q ` k ) = ( P ` 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 14 fveq1i 
 |-  ( Q ` k ) = ( ( P u. { <. ( N + 1 ) , C >. } ) ` k )
17 fzp1nel 
 |-  -. ( N + 1 ) e. ( 0 ... N )
18 eleq1 
 |-  ( k = ( N + 1 ) -> ( k e. ( 0 ... N ) <-> ( N + 1 ) e. ( 0 ... N ) ) )
19 18 notbid 
 |-  ( k = ( N + 1 ) -> ( -. k e. ( 0 ... N ) <-> -. ( N + 1 ) e. ( 0 ... N ) ) )
20 19 eqcoms 
 |-  ( ( N + 1 ) = k -> ( -. k e. ( 0 ... N ) <-> -. ( N + 1 ) e. ( 0 ... N ) ) )
21 17 20 mpbiri 
 |-  ( ( N + 1 ) = k -> -. k e. ( 0 ... N ) )
22 21 a1i 
 |-  ( ph -> ( ( N + 1 ) = k -> -. k e. ( 0 ... N ) ) )
23 22 con2d 
 |-  ( ph -> ( k e. ( 0 ... N ) -> -. ( N + 1 ) = k ) )
24 23 imp 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> -. ( N + 1 ) = k )
25 24 neqned 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( N + 1 ) =/= k )
26 fvunsn 
 |-  ( ( N + 1 ) =/= k -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` k ) = ( P ` k ) )
27 25 26 syl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` k ) = ( P ` k ) )
28 16 27 eqtrid 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( Q ` k ) = ( P ` k ) )
29 28 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ... N ) ( Q ` k ) = ( P ` k ) )