Metamath Proof Explorer

Theorem wwlksnextfun

Description: Lemma for wwlksnextbij . (Contributed by Alexander van der Vekens, 7-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnextbij0.v 
|- V = ( Vtx ` G )
wwlksnextbij0.e 
|- E = ( Edg ` G )
wwlksnextbij0.d 
|- D = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }
wwlksnextbij0.r 
|- R = { n e. V | { ( lastS ` W ) , n } e. E }
wwlksnextbij0.f 
|- F = ( t e. D |-> ( lastS ` t ) )
Assertion wwlksnextfun 
|- ( N e. NN0 -> F : D --> R )

Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v 
 |-  V = ( Vtx ` G )
2 wwlksnextbij0.e 
 |-  E = ( Edg ` G )
3 wwlksnextbij0.d 
 |-  D = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }
4 wwlksnextbij0.r 
 |-  R = { n e. V | { ( lastS ` W ) , n } e. E }
5 wwlksnextbij0.f 
 |-  F = ( t e. D |-> ( lastS ` t ) )
6 fveqeq2 
 |-  ( w = t -> ( ( # ` w ) = ( N + 2 ) <-> ( # ` t ) = ( N + 2 ) ) )
7 oveq1 
 |-  ( w = t -> ( w prefix ( N + 1 ) ) = ( t prefix ( N + 1 ) ) )
8 7 eqeq1d 
 |-  ( w = t -> ( ( w prefix ( N + 1 ) ) = W <-> ( t prefix ( N + 1 ) ) = W ) )
9 fveq2 
 |-  ( w = t -> ( lastS ` w ) = ( lastS ` t ) )
10 9 preq2d 
 |-  ( w = t -> { ( lastS ` W ) , ( lastS ` w ) } = { ( lastS ` W ) , ( lastS ` t ) } )
11 10 eleq1d 
 |-  ( w = t -> ( { ( lastS ` W ) , ( lastS ` w ) } e. E <-> { ( lastS ` W ) , ( lastS ` t ) } e. E ) )
12 6 8 11 3anbi123d 
 |-  ( w = t -> ( ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) <-> ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) ) )
13 12 3 elrab2 
 |-  ( t e. D <-> ( t e. Word V /\ ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) ) )
14 simpll 
 |-  ( ( ( t e. Word V /\ N e. NN0 ) /\ ( # ` t ) = ( N + 2 ) ) -> t e. Word V )
15 nn0re 
 |-  ( N e. NN0 -> N e. RR )
16 2re 
 |-  2 e. RR
17 16 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
18 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
19 2pos 
 |-  0 < 2
20 19 a1i 
 |-  ( N e. NN0 -> 0 < 2 )
21 15 17 18 20 addgegt0d 
 |-  ( N e. NN0 -> 0 < ( N + 2 ) )
22 21 ad2antlr 
 |-  ( ( ( t e. Word V /\ N e. NN0 ) /\ ( # ` t ) = ( N + 2 ) ) -> 0 < ( N + 2 ) )
23 breq2 
 |-  ( ( # ` t ) = ( N + 2 ) -> ( 0 < ( # ` t ) <-> 0 < ( N + 2 ) ) )
24 23 adantl 
 |-  ( ( ( t e. Word V /\ N e. NN0 ) /\ ( # ` t ) = ( N + 2 ) ) -> ( 0 < ( # ` t ) <-> 0 < ( N + 2 ) ) )
25 22 24 mpbird 
 |-  ( ( ( t e. Word V /\ N e. NN0 ) /\ ( # ` t ) = ( N + 2 ) ) -> 0 < ( # ` t ) )
26 hashgt0n0 
 |-  ( ( t e. Word V /\ 0 < ( # ` t ) ) -> t =/= (/) )
27 14 25 26 syl2anc 
 |-  ( ( ( t e. Word V /\ N e. NN0 ) /\ ( # ` t ) = ( N + 2 ) ) -> t =/= (/) )
28 14 27 jca 
 |-  ( ( ( t e. Word V /\ N e. NN0 ) /\ ( # ` t ) = ( N + 2 ) ) -> ( t e. Word V /\ t =/= (/) ) )
29 28 expcom 
 |-  ( ( # ` t ) = ( N + 2 ) -> ( ( t e. Word V /\ N e. NN0 ) -> ( t e. Word V /\ t =/= (/) ) ) )
30 29 3ad2ant1 
 |-  ( ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) -> ( ( t e. Word V /\ N e. NN0 ) -> ( t e. Word V /\ t =/= (/) ) ) )
31 30 expd 
 |-  ( ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) -> ( t e. Word V -> ( N e. NN0 -> ( t e. Word V /\ t =/= (/) ) ) ) )
32 31 impcom 
 |-  ( ( t e. Word V /\ ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) ) -> ( N e. NN0 -> ( t e. Word V /\ t =/= (/) ) ) )
33 32 impcom 
 |-  ( ( N e. NN0 /\ ( t e. Word V /\ ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) ) ) -> ( t e. Word V /\ t =/= (/) ) )
34 lswcl 
 |-  ( ( t e. Word V /\ t =/= (/) ) -> ( lastS ` t ) e. V )
35 33 34 syl 
 |-  ( ( N e. NN0 /\ ( t e. Word V /\ ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) ) ) -> ( lastS ` t ) e. V )
36 simprr3 
 |-  ( ( N e. NN0 /\ ( t e. Word V /\ ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) ) ) -> { ( lastS ` W ) , ( lastS ` t ) } e. E )
37 35 36 jca 
 |-  ( ( N e. NN0 /\ ( t e. Word V /\ ( ( # ` t ) = ( N + 2 ) /\ ( t prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) ) ) -> ( ( lastS ` t ) e. V /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) )
38 13 37 sylan2b 
 |-  ( ( N e. NN0 /\ t e. D ) -> ( ( lastS ` t ) e. V /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) )
39 preq2 
 |-  ( n = ( lastS ` t ) -> { ( lastS ` W ) , n } = { ( lastS ` W ) , ( lastS ` t ) } )
40 39 eleq1d 
 |-  ( n = ( lastS ` t ) -> ( { ( lastS ` W ) , n } e. E <-> { ( lastS ` W ) , ( lastS ` t ) } e. E ) )
41 40 4 elrab2 
 |-  ( ( lastS ` t ) e. R <-> ( ( lastS ` t ) e. V /\ { ( lastS ` W ) , ( lastS ` t ) } e. E ) )
42 38 41 sylibr 
 |-  ( ( N e. NN0 /\ t e. D ) -> ( lastS ` t ) e. R )
43 42 5 fmptd 
 |-  ( N e. NN0 -> F : D --> R )