Metamath Proof Explorer


Theorem wlkp1lem7

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 wlkp1lem7
|- ( ph -> { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` N ) ) )

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 fveq2
 |-  ( k = N -> ( Q ` k ) = ( Q ` N ) )
17 fveq2
 |-  ( k = N -> ( P ` k ) = ( P ` N ) )
18 16 17 eqeq12d
 |-  ( k = N -> ( ( Q ` k ) = ( P ` k ) <-> ( Q ` N ) = ( P ` N ) ) )
19 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem5
 |-  ( ph -> A. k e. ( 0 ... N ) ( Q ` k ) = ( P ` k ) )
20 wlkcl
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
21 9 eqcomi
 |-  ( # ` F ) = N
22 21 eleq1i
 |-  ( ( # ` F ) e. NN0 <-> N e. NN0 )
23 nn0fz0
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
24 22 23 sylbb
 |-  ( ( # ` F ) e. NN0 -> N e. ( 0 ... N ) )
25 8 20 24 3syl
 |-  ( ph -> N e. ( 0 ... N ) )
26 18 19 25 rspcdva
 |-  ( ph -> ( Q ` N ) = ( P ` N ) )
27 14 fveq1i
 |-  ( Q ` ( N + 1 ) ) = ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) )
28 ovex
 |-  ( N + 1 ) e. _V
29 1 2 3 4 5 6 7 8 9 wlkp1lem1
 |-  ( ph -> -. ( N + 1 ) e. dom P )
30 fsnunfv
 |-  ( ( ( N + 1 ) e. _V /\ C e. V /\ -. ( N + 1 ) e. dom P ) -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) = C )
31 28 6 29 30 mp3an2i
 |-  ( ph -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) = C )
32 27 31 syl5eq
 |-  ( ph -> ( Q ` ( N + 1 ) ) = C )
33 26 32 preq12d
 |-  ( ph -> { ( Q ` N ) , ( Q ` ( N + 1 ) ) } = { ( P ` N ) , C } )
34 fsnunfv
 |-  ( ( B e. W /\ E e. ( Edg ` G ) /\ -. B e. dom I ) -> ( ( I u. { <. B , E >. } ) ` B ) = E )
35 5 10 7 34 syl3anc
 |-  ( ph -> ( ( I u. { <. B , E >. } ) ` B ) = E )
36 11 33 35 3sstr4d
 |-  ( ph -> { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( I u. { <. B , E >. } ) ` B ) )
37 1 2 3 4 5 6 7 8 9 10 11 12 13 wlkp1lem3
 |-  ( ph -> ( ( iEdg ` S ) ` ( H ` N ) ) = ( ( I u. { <. B , E >. } ) ` B ) )
38 36 37 sseqtrrd
 |-  ( ph -> { ( Q ` N ) , ( Q ` ( N + 1 ) ) } C_ ( ( iEdg ` S ) ` ( H ` N ) ) )