Metamath Proof Explorer

Theorem wwlksnextinj

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 wwlksnextinj 
|- ( N e. NN0 -> F : D -1-1-> 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 2 3 4 5 wwlksnextfun 
 |-  ( N e. NN0 -> F : D --> R )
7 fveq2 
 |-  ( t = d -> ( lastS ` t ) = ( lastS ` d ) )
8 fvex 
 |-  ( lastS ` d ) e. _V
9 7 5 8 fvmpt 
 |-  ( d e. D -> ( F ` d ) = ( lastS ` d ) )
10 fveq2 
 |-  ( t = x -> ( lastS ` t ) = ( lastS ` x ) )
11 fvex 
 |-  ( lastS ` x ) e. _V
12 10 5 11 fvmpt 
 |-  ( x e. D -> ( F ` x ) = ( lastS ` x ) )
13 9 12 eqeqan12d 
 |-  ( ( d e. D /\ x e. D ) -> ( ( F ` d ) = ( F ` x ) <-> ( lastS ` d ) = ( lastS ` x ) ) )
14 13 adantl 
 |-  ( ( N e. NN0 /\ ( d e. D /\ x e. D ) ) -> ( ( F ` d ) = ( F ` x ) <-> ( lastS ` d ) = ( lastS ` x ) ) )
15 fveqeq2 
 |-  ( w = d -> ( ( # ` w ) = ( N + 2 ) <-> ( # ` d ) = ( N + 2 ) ) )
16 oveq1 
 |-  ( w = d -> ( w prefix ( N + 1 ) ) = ( d prefix ( N + 1 ) ) )
17 16 eqeq1d 
 |-  ( w = d -> ( ( w prefix ( N + 1 ) ) = W <-> ( d prefix ( N + 1 ) ) = W ) )
18 fveq2 
 |-  ( w = d -> ( lastS ` w ) = ( lastS ` d ) )
19 18 preq2d 
 |-  ( w = d -> { ( lastS ` W ) , ( lastS ` w ) } = { ( lastS ` W ) , ( lastS ` d ) } )
20 19 eleq1d 
 |-  ( w = d -> ( { ( lastS ` W ) , ( lastS ` w ) } e. E <-> { ( lastS ` W ) , ( lastS ` d ) } e. E ) )
21 15 17 20 3anbi123d 
 |-  ( w = d -> ( ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) <-> ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) )
22 21 3 elrab2 
 |-  ( d e. D <-> ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) )
23 fveqeq2 
 |-  ( w = x -> ( ( # ` w ) = ( N + 2 ) <-> ( # ` x ) = ( N + 2 ) ) )
24 oveq1 
 |-  ( w = x -> ( w prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) )
25 24 eqeq1d 
 |-  ( w = x -> ( ( w prefix ( N + 1 ) ) = W <-> ( x prefix ( N + 1 ) ) = W ) )
26 fveq2 
 |-  ( w = x -> ( lastS ` w ) = ( lastS ` x ) )
27 26 preq2d 
 |-  ( w = x -> { ( lastS ` W ) , ( lastS ` w ) } = { ( lastS ` W ) , ( lastS ` x ) } )
28 27 eleq1d 
 |-  ( w = x -> ( { ( lastS ` W ) , ( lastS ` w ) } e. E <-> { ( lastS ` W ) , ( lastS ` x ) } e. E ) )
29 23 25 28 3anbi123d 
 |-  ( w = x -> ( ( ( # ` w ) = ( N + 2 ) /\ ( w prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) <-> ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) )
30 29 3 elrab2 
 |-  ( x e. D <-> ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) )
31 eqtr3 
 |-  ( ( ( # ` d ) = ( N + 2 ) /\ ( # ` x ) = ( N + 2 ) ) -> ( # ` d ) = ( # ` x ) )
32 31 expcom 
 |-  ( ( # ` x ) = ( N + 2 ) -> ( ( # ` d ) = ( N + 2 ) -> ( # ` d ) = ( # ` x ) ) )
33 32 3ad2ant1 
 |-  ( ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) -> ( ( # ` d ) = ( N + 2 ) -> ( # ` d ) = ( # ` x ) ) )
34 33 adantl 
 |-  ( ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) -> ( ( # ` d ) = ( N + 2 ) -> ( # ` d ) = ( # ` x ) ) )
35 34 com12 
 |-  ( ( # ` d ) = ( N + 2 ) -> ( ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) -> ( # ` d ) = ( # ` x ) ) )
36 35 3ad2ant1 
 |-  ( ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) -> ( ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) -> ( # ` d ) = ( # ` x ) ) )
37 36 adantl 
 |-  ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) -> ( ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) -> ( # ` d ) = ( # ` x ) ) )
38 37 imp 
 |-  ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) -> ( # ` d ) = ( # ` x ) )
39 38 adantr 
 |-  ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) -> ( # ` d ) = ( # ` x ) )
40 39 adantr 
 |-  ( ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) /\ ( lastS ` d ) = ( lastS ` x ) ) -> ( # ` d ) = ( # ` x ) )
41 simpr 
 |-  ( ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) /\ ( lastS ` d ) = ( lastS ` x ) ) -> ( lastS ` d ) = ( lastS ` x ) )
42 eqtr3 
 |-  ( ( ( d prefix ( N + 1 ) ) = W /\ ( x prefix ( N + 1 ) ) = W ) -> ( d prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) )
43 1e2m1 
 |-  1 = ( 2 - 1 )
44 43 a1i 
 |-  ( N e. NN0 -> 1 = ( 2 - 1 ) )
45 44 oveq2d 
 |-  ( N e. NN0 -> ( N + 1 ) = ( N + ( 2 - 1 ) ) )
46 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
47 2cnd 
 |-  ( N e. NN0 -> 2 e. CC )
48 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
49 46 47 48 addsubassd 
 |-  ( N e. NN0 -> ( ( N + 2 ) - 1 ) = ( N + ( 2 - 1 ) ) )
50 45 49 eqtr4d 
 |-  ( N e. NN0 -> ( N + 1 ) = ( ( N + 2 ) - 1 ) )
51 50 adantr 
 |-  ( ( N e. NN0 /\ ( # ` d ) = ( N + 2 ) ) -> ( N + 1 ) = ( ( N + 2 ) - 1 ) )
52 oveq1 
 |-  ( ( # ` d ) = ( N + 2 ) -> ( ( # ` d ) - 1 ) = ( ( N + 2 ) - 1 ) )
53 52 eqeq2d 
 |-  ( ( # ` d ) = ( N + 2 ) -> ( ( N + 1 ) = ( ( # ` d ) - 1 ) <-> ( N + 1 ) = ( ( N + 2 ) - 1 ) ) )
54 53 adantl 
 |-  ( ( N e. NN0 /\ ( # ` d ) = ( N + 2 ) ) -> ( ( N + 1 ) = ( ( # ` d ) - 1 ) <-> ( N + 1 ) = ( ( N + 2 ) - 1 ) ) )
55 51 54 mpbird 
 |-  ( ( N e. NN0 /\ ( # ` d ) = ( N + 2 ) ) -> ( N + 1 ) = ( ( # ` d ) - 1 ) )
56 oveq2 
 |-  ( ( N + 1 ) = ( ( # ` d ) - 1 ) -> ( d prefix ( N + 1 ) ) = ( d prefix ( ( # ` d ) - 1 ) ) )
57 oveq2 
 |-  ( ( N + 1 ) = ( ( # ` d ) - 1 ) -> ( x prefix ( N + 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) )
58 56 57 eqeq12d 
 |-  ( ( N + 1 ) = ( ( # ` d ) - 1 ) -> ( ( d prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) <-> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) )
59 55 58 syl 
 |-  ( ( N e. NN0 /\ ( # ` d ) = ( N + 2 ) ) -> ( ( d prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) <-> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) )
60 59 biimpd 
 |-  ( ( N e. NN0 /\ ( # ` d ) = ( N + 2 ) ) -> ( ( d prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) )
61 60 ex 
 |-  ( N e. NN0 -> ( ( # ` d ) = ( N + 2 ) -> ( ( d prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
62 61 com13 
 |-  ( ( d prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) -> ( ( # ` d ) = ( N + 2 ) -> ( N e. NN0 -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
63 42 62 syl 
 |-  ( ( ( d prefix ( N + 1 ) ) = W /\ ( x prefix ( N + 1 ) ) = W ) -> ( ( # ` d ) = ( N + 2 ) -> ( N e. NN0 -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
64 63 ex 
 |-  ( ( d prefix ( N + 1 ) ) = W -> ( ( x prefix ( N + 1 ) ) = W -> ( ( # ` d ) = ( N + 2 ) -> ( N e. NN0 -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) ) )
65 64 com23 
 |-  ( ( d prefix ( N + 1 ) ) = W -> ( ( # ` d ) = ( N + 2 ) -> ( ( x prefix ( N + 1 ) ) = W -> ( N e. NN0 -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) ) )
66 65 impcom 
 |-  ( ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W ) -> ( ( x prefix ( N + 1 ) ) = W -> ( N e. NN0 -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
67 66 com12 
 |-  ( ( x prefix ( N + 1 ) ) = W -> ( ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W ) -> ( N e. NN0 -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
68 67 3ad2ant2 
 |-  ( ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) -> ( ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W ) -> ( N e. NN0 -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
69 68 adantl 
 |-  ( ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) -> ( ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W ) -> ( N e. NN0 -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
70 69 com12 
 |-  ( ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W ) -> ( ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) -> ( N e. NN0 -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
71 70 3adant3 
 |-  ( ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) -> ( ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) -> ( N e. NN0 -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
72 71 adantl 
 |-  ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) -> ( ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) -> ( N e. NN0 -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
73 72 imp31 
 |-  ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) )
74 73 adantr 
 |-  ( ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) /\ ( lastS ` d ) = ( lastS ` x ) ) -> ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) )
75 simpl 
 |-  ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) -> d e. Word V )
76 simpl 
 |-  ( ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) -> x e. Word V )
77 75 76 anim12i 
 |-  ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) -> ( d e. Word V /\ x e. Word V ) )
78 77 adantr 
 |-  ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) -> ( d e. Word V /\ x e. Word V ) )
79 nn0re 
 |-  ( N e. NN0 -> N e. RR )
80 2re 
 |-  2 e. RR
81 80 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
82 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
83 2pos 
 |-  0 < 2
84 83 a1i 
 |-  ( N e. NN0 -> 0 < 2 )
85 79 81 82 84 addgegt0d 
 |-  ( N e. NN0 -> 0 < ( N + 2 ) )
86 85 adantl 
 |-  ( ( ( # ` d ) = ( N + 2 ) /\ N e. NN0 ) -> 0 < ( N + 2 ) )
87 breq2 
 |-  ( ( # ` d ) = ( N + 2 ) -> ( 0 < ( # ` d ) <-> 0 < ( N + 2 ) ) )
88 87 adantr 
 |-  ( ( ( # ` d ) = ( N + 2 ) /\ N e. NN0 ) -> ( 0 < ( # ` d ) <-> 0 < ( N + 2 ) ) )
89 86 88 mpbird 
 |-  ( ( ( # ` d ) = ( N + 2 ) /\ N e. NN0 ) -> 0 < ( # ` d ) )
90 hashgt0n0 
 |-  ( ( d e. Word V /\ 0 < ( # ` d ) ) -> d =/= (/) )
91 89 90 sylan2 
 |-  ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ N e. NN0 ) ) -> d =/= (/) )
92 91 exp32 
 |-  ( d e. Word V -> ( ( # ` d ) = ( N + 2 ) -> ( N e. NN0 -> d =/= (/) ) ) )
93 92 com12 
 |-  ( ( # ` d ) = ( N + 2 ) -> ( d e. Word V -> ( N e. NN0 -> d =/= (/) ) ) )
94 93 3ad2ant1 
 |-  ( ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) -> ( d e. Word V -> ( N e. NN0 -> d =/= (/) ) ) )
95 94 impcom 
 |-  ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) -> ( N e. NN0 -> d =/= (/) ) )
96 95 adantr 
 |-  ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) -> ( N e. NN0 -> d =/= (/) ) )
97 96 imp 
 |-  ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) -> d =/= (/) )
98 85 adantl 
 |-  ( ( ( # ` x ) = ( N + 2 ) /\ N e. NN0 ) -> 0 < ( N + 2 ) )
99 breq2 
 |-  ( ( # ` x ) = ( N + 2 ) -> ( 0 < ( # ` x ) <-> 0 < ( N + 2 ) ) )
100 99 adantr 
 |-  ( ( ( # ` x ) = ( N + 2 ) /\ N e. NN0 ) -> ( 0 < ( # ` x ) <-> 0 < ( N + 2 ) ) )
101 98 100 mpbird 
 |-  ( ( ( # ` x ) = ( N + 2 ) /\ N e. NN0 ) -> 0 < ( # ` x ) )
102 hashgt0n0 
 |-  ( ( x e. Word V /\ 0 < ( # ` x ) ) -> x =/= (/) )
103 101 102 sylan2 
 |-  ( ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ N e. NN0 ) ) -> x =/= (/) )
104 103 exp32 
 |-  ( x e. Word V -> ( ( # ` x ) = ( N + 2 ) -> ( N e. NN0 -> x =/= (/) ) ) )
105 104 com12 
 |-  ( ( # ` x ) = ( N + 2 ) -> ( x e. Word V -> ( N e. NN0 -> x =/= (/) ) ) )
106 105 3ad2ant1 
 |-  ( ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) -> ( x e. Word V -> ( N e. NN0 -> x =/= (/) ) ) )
107 106 impcom 
 |-  ( ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) -> ( N e. NN0 -> x =/= (/) ) )
108 107 adantl 
 |-  ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) -> ( N e. NN0 -> x =/= (/) ) )
109 108 imp 
 |-  ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) -> x =/= (/) )
110 78 97 109 jca32 
 |-  ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) -> ( ( d e. Word V /\ x e. Word V ) /\ ( d =/= (/) /\ x =/= (/) ) ) )
111 110 adantr 
 |-  ( ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) /\ ( lastS ` d ) = ( lastS ` x ) ) -> ( ( d e. Word V /\ x e. Word V ) /\ ( d =/= (/) /\ x =/= (/) ) ) )
112 simpl 
 |-  ( ( d e. Word V /\ x e. Word V ) -> d e. Word V )
113 112 adantr 
 |-  ( ( ( d e. Word V /\ x e. Word V ) /\ ( d =/= (/) /\ x =/= (/) ) ) -> d e. Word V )
114 simpr 
 |-  ( ( d e. Word V /\ x e. Word V ) -> x e. Word V )
115 114 adantr 
 |-  ( ( ( d e. Word V /\ x e. Word V ) /\ ( d =/= (/) /\ x =/= (/) ) ) -> x e. Word V )
116 hashneq0 
 |-  ( d e. Word V -> ( 0 < ( # ` d ) <-> d =/= (/) ) )
117 116 biimprd 
 |-  ( d e. Word V -> ( d =/= (/) -> 0 < ( # ` d ) ) )
118 117 adantr 
 |-  ( ( d e. Word V /\ x e. Word V ) -> ( d =/= (/) -> 0 < ( # ` d ) ) )
119 118 com12 
 |-  ( d =/= (/) -> ( ( d e. Word V /\ x e. Word V ) -> 0 < ( # ` d ) ) )
120 119 adantr 
 |-  ( ( d =/= (/) /\ x =/= (/) ) -> ( ( d e. Word V /\ x e. Word V ) -> 0 < ( # ` d ) ) )
121 120 impcom 
 |-  ( ( ( d e. Word V /\ x e. Word V ) /\ ( d =/= (/) /\ x =/= (/) ) ) -> 0 < ( # ` d ) )
122 pfxsuff1eqwrdeq 
 |-  ( ( d e. Word V /\ x e. Word V /\ 0 < ( # ` d ) ) -> ( d = x <-> ( ( # ` d ) = ( # ` x ) /\ ( ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) /\ ( lastS ` d ) = ( lastS ` x ) ) ) ) )
123 113 115 121 122 syl3anc 
 |-  ( ( ( d e. Word V /\ x e. Word V ) /\ ( d =/= (/) /\ x =/= (/) ) ) -> ( d = x <-> ( ( # ` d ) = ( # ` x ) /\ ( ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) /\ ( lastS ` d ) = ( lastS ` x ) ) ) ) )
124 ancom 
 |-  ( ( ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) /\ ( lastS ` d ) = ( lastS ` x ) ) <-> ( ( lastS ` d ) = ( lastS ` x ) /\ ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) )
125 124 anbi2i 
 |-  ( ( ( # ` d ) = ( # ` x ) /\ ( ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) /\ ( lastS ` d ) = ( lastS ` x ) ) ) <-> ( ( # ` d ) = ( # ` x ) /\ ( ( lastS ` d ) = ( lastS ` x ) /\ ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
126 3anass 
 |-  ( ( ( # ` d ) = ( # ` x ) /\ ( lastS ` d ) = ( lastS ` x ) /\ ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) <-> ( ( # ` d ) = ( # ` x ) /\ ( ( lastS ` d ) = ( lastS ` x ) /\ ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
127 125 126 bitr4i 
 |-  ( ( ( # ` d ) = ( # ` x ) /\ ( ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) /\ ( lastS ` d ) = ( lastS ` x ) ) ) <-> ( ( # ` d ) = ( # ` x ) /\ ( lastS ` d ) = ( lastS ` x ) /\ ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) )
128 123 127 bitrdi 
 |-  ( ( ( d e. Word V /\ x e. Word V ) /\ ( d =/= (/) /\ x =/= (/) ) ) -> ( d = x <-> ( ( # ` d ) = ( # ` x ) /\ ( lastS ` d ) = ( lastS ` x ) /\ ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
129 111 128 syl 
 |-  ( ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) /\ ( lastS ` d ) = ( lastS ` x ) ) -> ( d = x <-> ( ( # ` d ) = ( # ` x ) /\ ( lastS ` d ) = ( lastS ` x ) /\ ( d prefix ( ( # ` d ) - 1 ) ) = ( x prefix ( ( # ` d ) - 1 ) ) ) ) )
130 40 41 74 129 mpbir3and 
 |-  ( ( ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) /\ N e. NN0 ) /\ ( lastS ` d ) = ( lastS ` x ) ) -> d = x )
131 130 exp31 
 |-  ( ( ( d e. Word V /\ ( ( # ` d ) = ( N + 2 ) /\ ( d prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` d ) } e. E ) ) /\ ( x e. Word V /\ ( ( # ` x ) = ( N + 2 ) /\ ( x prefix ( N + 1 ) ) = W /\ { ( lastS ` W ) , ( lastS ` x ) } e. E ) ) ) -> ( N e. NN0 -> ( ( lastS ` d ) = ( lastS ` x ) -> d = x ) ) )
132 22 30 131 syl2anb 
 |-  ( ( d e. D /\ x e. D ) -> ( N e. NN0 -> ( ( lastS ` d ) = ( lastS ` x ) -> d = x ) ) )
133 132 impcom 
 |-  ( ( N e. NN0 /\ ( d e. D /\ x e. D ) ) -> ( ( lastS ` d ) = ( lastS ` x ) -> d = x ) )
134 14 133 sylbid 
 |-  ( ( N e. NN0 /\ ( d e. D /\ x e. D ) ) -> ( ( F ` d ) = ( F ` x ) -> d = x ) )
135 134 ralrimivva 
 |-  ( N e. NN0 -> A. d e. D A. x e. D ( ( F ` d ) = ( F ` x ) -> d = x ) )
136 dff13 
 |-  ( F : D -1-1-> R <-> ( F : D --> R /\ A. d e. D A. x e. D ( ( F ` d ) = ( F ` x ) -> d = x ) ) )
137 6 135 136 sylanbrc 
 |-  ( N e. NN0 -> F : D -1-1-> R )