Metamath Proof Explorer

Theorem wlkp1lem2

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 >. } )
Assertion wlkp1lem2 
|- ( ph -> ( # ` H ) = ( N + 1 ) )

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 13 fveq2i 
 |-  ( # ` H ) = ( # ` ( F u. { <. N , B >. } ) )
15 14 a1i 
 |-  ( ph -> ( # ` H ) = ( # ` ( F u. { <. N , B >. } ) ) )
16 opex 
 |-  <. N , B >. e. _V
17 2 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
18 wrdfin 
 |-  ( F e. Word dom I -> F e. Fin )
19 8 17 18 3syl 
 |-  ( ph -> F e. Fin )
20 fzonel 
 |-  -. ( # ` F ) e. ( 0 ..^ ( # ` F ) )
21 20 a1i 
 |-  ( ph -> -. ( # ` F ) e. ( 0 ..^ ( # ` F ) ) )
22 eleq1 
 |-  ( N = ( # ` F ) -> ( N e. ( 0 ..^ ( # ` F ) ) <-> ( # ` F ) e. ( 0 ..^ ( # ` F ) ) ) )
23 22 notbid 
 |-  ( N = ( # ` F ) -> ( -. N e. ( 0 ..^ ( # ` F ) ) <-> -. ( # ` F ) e. ( 0 ..^ ( # ` F ) ) ) )
24 21 23 syl5ibr 
 |-  ( N = ( # ` F ) -> ( ph -> -. N e. ( 0 ..^ ( # ` F ) ) ) )
25 9 24 ax-mp 
 |-  ( ph -> -. N e. ( 0 ..^ ( # ` F ) ) )
26 wrdfn 
 |-  ( F e. Word dom I -> F Fn ( 0 ..^ ( # ` F ) ) )
27 8 17 26 3syl 
 |-  ( ph -> F Fn ( 0 ..^ ( # ` F ) ) )
28 fnop 
 |-  ( ( F Fn ( 0 ..^ ( # ` F ) ) /\ <. N , B >. e. F ) -> N e. ( 0 ..^ ( # ` F ) ) )
29 28 ex 
 |-  ( F Fn ( 0 ..^ ( # ` F ) ) -> ( <. N , B >. e. F -> N e. ( 0 ..^ ( # ` F ) ) ) )
30 27 29 syl 
 |-  ( ph -> ( <. N , B >. e. F -> N e. ( 0 ..^ ( # ` F ) ) ) )
31 25 30 mtod 
 |-  ( ph -> -. <. N , B >. e. F )
32 19 31 jca 
 |-  ( ph -> ( F e. Fin /\ -. <. N , B >. e. F ) )
33 hashunsng 
 |-  ( <. N , B >. e. _V -> ( ( F e. Fin /\ -. <. N , B >. e. F ) -> ( # ` ( F u. { <. N , B >. } ) ) = ( ( # ` F ) + 1 ) ) )
34 16 32 33 mpsyl 
 |-  ( ph -> ( # ` ( F u. { <. N , B >. } ) ) = ( ( # ` F ) + 1 ) )
35 9 eqcomi 
 |-  ( # ` F ) = N
36 35 a1i 
 |-  ( ph -> ( # ` F ) = N )
37 36 oveq1d 
 |-  ( ph -> ( ( # ` F ) + 1 ) = ( N + 1 ) )
38 15 34 37 3eqtrd 
 |-  ( ph -> ( # ` H ) = ( N + 1 ) )