Metamath Proof Explorer

Theorem wwlksnextsurj

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 wwlksnextsurj 
|- ( W e. ( N WWalksN G ) -> F : D -onto-> 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 1 wwlknbp 
 |-  ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) )
7 simp2 
 |-  ( ( G e. _V /\ N e. NN0 /\ W e. Word V ) -> N e. NN0 )
8 1 2 3 4 5 wwlksnextfun 
 |-  ( N e. NN0 -> F : D --> R )
9 6 7 8 3syl 
 |-  ( W e. ( N WWalksN G ) -> F : D --> R )
10 preq2 
 |-  ( n = r -> { ( lastS ` W ) , n } = { ( lastS ` W ) , r } )
11 10 eleq1d 
 |-  ( n = r -> ( { ( lastS ` W ) , n } e. E <-> { ( lastS ` W ) , r } e. E ) )
12 11 4 elrab2 
 |-  ( r e. R <-> ( r e. V /\ { ( lastS ` W ) , r } e. E ) )
13 1 2 wwlksnext 
 |-  ( ( W e. ( N WWalksN G ) /\ r e. V /\ { ( lastS ` W ) , r } e. E ) -> ( W ++ <" r "> ) e. ( ( N + 1 ) WWalksN G ) )
14 13 3expb 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> ( W ++ <" r "> ) e. ( ( N + 1 ) WWalksN G ) )
15 s1cl 
 |-  ( r e. V -> <" r "> e. Word V )
16 pfxccat1 
 |-  ( ( W e. Word V /\ <" r "> e. Word V ) -> ( ( W ++ <" r "> ) prefix ( # ` W ) ) = W )
17 15 16 sylan2 
 |-  ( ( W e. Word V /\ r e. V ) -> ( ( W ++ <" r "> ) prefix ( # ` W ) ) = W )
18 17 ex 
 |-  ( W e. Word V -> ( r e. V -> ( ( W ++ <" r "> ) prefix ( # ` W ) ) = W ) )
19 18 adantr 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( r e. V -> ( ( W ++ <" r "> ) prefix ( # ` W ) ) = W ) )
20 oveq2 
 |-  ( ( N + 1 ) = ( # ` W ) -> ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = ( ( W ++ <" r "> ) prefix ( # ` W ) ) )
21 20 eqcoms 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = ( ( W ++ <" r "> ) prefix ( # ` W ) ) )
22 21 eqeq1d 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W <-> ( ( W ++ <" r "> ) prefix ( # ` W ) ) = W ) )
23 22 adantl 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W <-> ( ( W ++ <" r "> ) prefix ( # ` W ) ) = W ) )
24 19 23 sylibrd 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) ) -> ( r e. V -> ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W ) )
25 24 3adant3 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( r e. V -> ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W ) )
26 1 2 wwlknp 
 |-  ( W e. ( N WWalksN G ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
27 25 26 syl11 
 |-  ( r e. V -> ( W e. ( N WWalksN G ) -> ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W ) )
28 27 adantr 
 |-  ( ( r e. V /\ { ( lastS ` W ) , r } e. E ) -> ( W e. ( N WWalksN G ) -> ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W ) )
29 28 impcom 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W )
30 lswccats1 
 |-  ( ( W e. Word V /\ r e. V ) -> ( lastS ` ( W ++ <" r "> ) ) = r )
31 30 eqcomd 
 |-  ( ( W e. Word V /\ r e. V ) -> r = ( lastS ` ( W ++ <" r "> ) ) )
32 31 ex 
 |-  ( W e. Word V -> ( r e. V -> r = ( lastS ` ( W ++ <" r "> ) ) ) )
33 32 3ad2ant3 
 |-  ( ( G e. _V /\ N e. NN0 /\ W e. Word V ) -> ( r e. V -> r = ( lastS ` ( W ++ <" r "> ) ) ) )
34 6 33 syl 
 |-  ( W e. ( N WWalksN G ) -> ( r e. V -> r = ( lastS ` ( W ++ <" r "> ) ) ) )
35 34 imp 
 |-  ( ( W e. ( N WWalksN G ) /\ r e. V ) -> r = ( lastS ` ( W ++ <" r "> ) ) )
36 35 preq2d 
 |-  ( ( W e. ( N WWalksN G ) /\ r e. V ) -> { ( lastS ` W ) , r } = { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } )
37 36 eleq1d 
 |-  ( ( W e. ( N WWalksN G ) /\ r e. V ) -> ( { ( lastS ` W ) , r } e. E <-> { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E ) )
38 37 biimpd 
 |-  ( ( W e. ( N WWalksN G ) /\ r e. V ) -> ( { ( lastS ` W ) , r } e. E -> { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E ) )
39 38 impr 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E )
40 14 29 39 jca32 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> ( ( W ++ <" r "> ) e. ( ( N + 1 ) WWalksN G ) /\ ( ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E ) ) )
41 33 6 syl11 
 |-  ( r e. V -> ( W e. ( N WWalksN G ) -> r = ( lastS ` ( W ++ <" r "> ) ) ) )
42 41 adantr 
 |-  ( ( r e. V /\ { ( lastS ` W ) , r } e. E ) -> ( W e. ( N WWalksN G ) -> r = ( lastS ` ( W ++ <" r "> ) ) ) )
43 42 impcom 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> r = ( lastS ` ( W ++ <" r "> ) ) )
44 ovexd 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> ( W ++ <" r "> ) e. _V )
45 eleq1 
 |-  ( d = ( W ++ <" r "> ) -> ( d e. ( ( N + 1 ) WWalksN G ) <-> ( W ++ <" r "> ) e. ( ( N + 1 ) WWalksN G ) ) )
46 oveq1 
 |-  ( d = ( W ++ <" r "> ) -> ( d prefix ( N + 1 ) ) = ( ( W ++ <" r "> ) prefix ( N + 1 ) ) )
47 46 eqeq1d 
 |-  ( d = ( W ++ <" r "> ) -> ( ( d prefix ( N + 1 ) ) = W <-> ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W ) )
48 fveq2 
 |-  ( d = ( W ++ <" r "> ) -> ( lastS ` d ) = ( lastS ` ( W ++ <" r "> ) ) )
49 48 preq2d 
 |-  ( d = ( W ++ <" r "> ) -> { ( lastS ` W ) , ( lastS ` d ) } = { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } )
50 49 eleq1d 
 |-  ( d = ( W ++ <" r "> ) -> ( { ( lastS ` W ) , ( lastS ` d ) } e. E <-> { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E ) )
51 47 50 anbi12d 
 |-  ( d = ( W ++ <" r "> ) -> ( ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) <-> ( ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E ) ) )
52 45 51 anbi12d 
 |-  ( d = ( W ++ <" r "> ) -> ( ( d e. ( ( N + 1 ) WWalksN G ) /\ ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) <-> ( ( W ++ <" r "> ) e. ( ( N + 1 ) WWalksN G ) /\ ( ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E ) ) ) )
53 48 eqeq2d 
 |-  ( d = ( W ++ <" r "> ) -> ( r = ( lastS ` d ) <-> r = ( lastS ` ( W ++ <" r "> ) ) ) )
54 52 53 anbi12d 
 |-  ( d = ( W ++ <" r "> ) -> ( ( ( d e. ( ( N + 1 ) WWalksN G ) /\ ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ r = ( lastS ` d ) ) <-> ( ( ( W ++ <" r "> ) e. ( ( N + 1 ) WWalksN G ) /\ ( ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E ) ) /\ r = ( lastS ` ( W ++ <" r "> ) ) ) ) )
55 54 bicomd 
 |-  ( d = ( W ++ <" r "> ) -> ( ( ( ( W ++ <" r "> ) e. ( ( N + 1 ) WWalksN G ) /\ ( ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E ) ) /\ r = ( lastS ` ( W ++ <" r "> ) ) ) <-> ( ( d e. ( ( N + 1 ) WWalksN G ) /\ ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ r = ( lastS ` d ) ) ) )
56 55 adantl 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) /\ d = ( W ++ <" r "> ) ) -> ( ( ( ( W ++ <" r "> ) e. ( ( N + 1 ) WWalksN G ) /\ ( ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E ) ) /\ r = ( lastS ` ( W ++ <" r "> ) ) ) <-> ( ( d e. ( ( N + 1 ) WWalksN G ) /\ ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ r = ( lastS ` d ) ) ) )
57 56 biimpd 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) /\ d = ( W ++ <" r "> ) ) -> ( ( ( ( W ++ <" r "> ) e. ( ( N + 1 ) WWalksN G ) /\ ( ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E ) ) /\ r = ( lastS ` ( W ++ <" r "> ) ) ) -> ( ( d e. ( ( N + 1 ) WWalksN G ) /\ ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ r = ( lastS ` d ) ) ) )
58 44 57 spcimedv 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> ( ( ( ( W ++ <" r "> ) e. ( ( N + 1 ) WWalksN G ) /\ ( ( ( W ++ <" r "> ) prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` ( W ++ <" r "> ) ) } e. E ) ) /\ r = ( lastS ` ( W ++ <" r "> ) ) ) -> E. d ( ( d e. ( ( N + 1 ) WWalksN G ) /\ ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ r = ( lastS ` d ) ) ) )
59 40 43 58 mp2and 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> E. d ( ( d e. ( ( N + 1 ) WWalksN G ) /\ ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ r = ( lastS ` d ) ) )
60 oveq1 
 |-  ( w = d -> ( w prefix ( N + 1 ) ) = ( d prefix ( N + 1 ) ) )
61 60 eqeq1d 
 |-  ( w = d -> ( ( w prefix ( N + 1 ) ) = W <-> ( d prefix ( N + 1 ) ) = W ) )
62 fveq2 
 |-  ( w = d -> ( lastS ` w ) = ( lastS ` d ) )
63 62 preq2d 
 |-  ( w = d -> { ( lastS ` W ) , ( lastS ` w ) } = { ( lastS ` W ) , ( lastS ` d ) } )
64 63 eleq1d 
 |-  ( w = d -> ( { ( lastS ` W ) , ( lastS ` w ) } e. E <-> { ( lastS ` W ) , ( lastS ` d ) } e. E ) )
65 61 64 anbi12d 
 |-  ( w = d -> ( ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) <-> ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) )
66 65 elrab 
 |-  ( d e. { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } <-> ( d e. ( ( N + 1 ) WWalksN G ) /\ ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) )
67 66 anbi1i 
 |-  ( ( d e. { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } /\ r = ( lastS ` d ) ) <-> ( ( d e. ( ( N + 1 ) WWalksN G ) /\ ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ r = ( lastS ` d ) ) )
68 67 exbii 
 |-  ( E. d ( d e. { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } /\ r = ( lastS ` d ) ) <-> E. d ( ( d e. ( ( N + 1 ) WWalksN G ) /\ ( ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ r = ( lastS ` d ) ) )
69 59 68 sylibr 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> E. d ( d e. { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } /\ r = ( lastS ` d ) ) )
70 df-rex 
 |-  ( E. d e. { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } r = ( lastS ` d ) <-> E. d ( d e. { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } /\ r = ( lastS ` d ) ) )
71 69 70 sylibr 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> E. d e. { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } r = ( lastS ` d ) )
72 1 2 3 wwlksnextwrd 
 |-  ( W e. ( N WWalksN G ) -> D = { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } )
73 72 adantr 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> D = { w e. ( ( N + 1 ) WWalksN G ) | ( ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } )
74 71 73 rexeqtrrdv 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> E. d e. D r = ( lastS ` d ) )
75 fveq2 
 |-  ( t = d -> ( lastS ` t ) = ( lastS ` d ) )
76 fvex 
 |-  ( lastS ` d ) e. _V
77 75 5 76 fvmpt 
 |-  ( d e. D -> ( F ` d ) = ( lastS ` d ) )
78 77 eqeq2d 
 |-  ( d e. D -> ( r = ( F ` d ) <-> r = ( lastS ` d ) ) )
79 78 rexbiia 
 |-  ( E. d e. D r = ( F ` d ) <-> E. d e. D r = ( lastS ` d ) )
80 74 79 sylibr 
 |-  ( ( W e. ( N WWalksN G ) /\ ( r e. V /\ { ( lastS ` W ) , r } e. E ) ) -> E. d e. D r = ( F ` d ) )
81 12 80 sylan2b 
 |-  ( ( W e. ( N WWalksN G ) /\ r e. R ) -> E. d e. D r = ( F ` d ) )
82 81 ralrimiva 
 |-  ( W e. ( N WWalksN G ) -> A. r e. R E. d e. D r = ( F ` d ) )
83 dffo3 
 |-  ( F : D -onto-> R <-> ( F : D --> R /\ A. r e. R E. d e. D r = ( F ` d ) ) )
84 9 82 83 sylanbrc 
 |-  ( W e. ( N WWalksN G ) -> F : D -onto-> R )