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 Word V | w = N + 2 w prefix N + 1 = W lastS W lastS w E
wwlksnextbij0.r R = n V | lastS W n E
wwlksnextbij0.f F = t D lastS t
Assertion wwlksnextinj N 0 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 Word V | w = N + 2 w prefix N + 1 = W lastS W lastS w E
4 wwlksnextbij0.r R = n V | lastS W n E
5 wwlksnextbij0.f F = t D lastS t
6 1 2 3 4 5 wwlksnextfun N 0 F : D R
7 fveq2 t = d lastS t = lastS d
8 fvex lastS d V
9 7 5 8 fvmpt d D F d = lastS d
10 fveq2 t = x lastS t = lastS x
11 fvex lastS x V
12 10 5 11 fvmpt x D F x = lastS x
13 9 12 eqeqan12d d D x D F d = F x lastS d = lastS x
14 13 adantl N 0 d D x 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 lastS W lastS d E
21 15 17 20 3anbi123d w = d w = N + 2 w prefix N + 1 = W lastS W lastS w E d = N + 2 d prefix N + 1 = W lastS W lastS d E
22 21 3 elrab2 d D d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d 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 lastS W lastS x E
29 23 25 28 3anbi123d w = x w = N + 2 w prefix N + 1 = W lastS W lastS w E x = N + 2 x prefix N + 1 = W lastS W lastS x E
30 29 3 elrab2 x D x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x 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 d = N + 2 d = x
34 33 adantl x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E d = N + 2 d = x
35 34 com12 d = N + 2 x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E d = x
36 35 3ad2ant1 d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E d = x
37 36 adantl d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E d = x
38 37 imp d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E d = x
39 38 adantr d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 d = x
40 39 adantr d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 lastS d = lastS x d = x
41 simpr d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 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 0 1 = 2 1
45 44 oveq2d N 0 N + 1 = N + 2 - 1
46 nn0cn N 0 N
47 2cnd N 0 2
48 1cnd N 0 1
49 46 47 48 addsubassd N 0 N + 2 - 1 = N + 2 - 1
50 45 49 eqtr4d N 0 N + 1 = N + 2 - 1
51 50 adantr N 0 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 0 d = N + 2 N + 1 = d 1 N + 1 = N + 2 - 1
55 51 54 mpbird N 0 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 0 d = N + 2 d prefix N + 1 = x prefix N + 1 d prefix d 1 = x prefix d 1
60 59 biimpd N 0 d = N + 2 d prefix N + 1 = x prefix N + 1 d prefix d 1 = x prefix d 1
61 60 ex N 0 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 0 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 0 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 0 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 0 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 0 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 0 d prefix d 1 = x prefix d 1
68 67 3ad2ant2 x = N + 2 x prefix N + 1 = W lastS W lastS x E d = N + 2 d prefix N + 1 = W N 0 d prefix d 1 = x prefix d 1
69 68 adantl x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E d = N + 2 d prefix N + 1 = W N 0 d prefix d 1 = x prefix d 1
70 69 com12 d = N + 2 d prefix N + 1 = W x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 d prefix d 1 = x prefix d 1
71 70 3adant3 d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 d prefix d 1 = x prefix d 1
72 71 adantl d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 d prefix d 1 = x prefix d 1
73 72 imp31 d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 d prefix d 1 = x prefix d 1
74 73 adantr d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 lastS d = lastS x d prefix d 1 = x prefix d 1
75 simpl d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E d Word V
76 simpl x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E x Word V
77 75 76 anim12i d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E d Word V x Word V
78 77 adantr d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 d Word V x Word V
79 nn0re N 0 N
80 2re 2
81 80 a1i N 0 2
82 nn0ge0 N 0 0 N
83 2pos 0 < 2
84 83 a1i N 0 0 < 2
85 79 81 82 84 addgegt0d N 0 0 < N + 2
86 85 adantl d = N + 2 N 0 0 < N + 2
87 breq2 d = N + 2 0 < d 0 < N + 2
88 87 adantr d = N + 2 N 0 0 < d 0 < N + 2
89 86 88 mpbird d = N + 2 N 0 0 < d
90 hashgt0n0 d Word V 0 < d d
91 89 90 sylan2 d Word V d = N + 2 N 0 d
92 91 exp32 d Word V d = N + 2 N 0 d
93 92 com12 d = N + 2 d Word V N 0 d
94 93 3ad2ant1 d = N + 2 d prefix N + 1 = W lastS W lastS d E d Word V N 0 d
95 94 impcom d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E N 0 d
96 95 adantr d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 d
97 96 imp d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 d
98 85 adantl x = N + 2 N 0 0 < N + 2
99 breq2 x = N + 2 0 < x 0 < N + 2
100 99 adantr x = N + 2 N 0 0 < x 0 < N + 2
101 98 100 mpbird x = N + 2 N 0 0 < x
102 hashgt0n0 x Word V 0 < x x
103 101 102 sylan2 x Word V x = N + 2 N 0 x
104 103 exp32 x Word V x = N + 2 N 0 x
105 104 com12 x = N + 2 x Word V N 0 x
106 105 3ad2ant1 x = N + 2 x prefix N + 1 = W lastS W lastS x E x Word V N 0 x
107 106 impcom x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 x
108 107 adantl d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 x
109 108 imp d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 x
110 78 97 109 jca32 d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 d Word V x Word V d x
111 110 adantr d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 lastS d = lastS x d Word V x Word V d x
112 simpl d Word V x Word V d Word V
113 112 adantr d Word V x Word V d x d Word V
114 simpr d Word V x Word V x Word V
115 114 adantr d Word V x Word V d x x Word V
116 hashneq0 d Word V 0 < d d
117 116 biimprd d Word V d 0 < d
118 117 adantr d Word V x Word V d 0 < d
119 118 com12 d d Word V x Word V 0 < d
120 119 adantr d x d Word V x Word V 0 < d
121 120 impcom d Word V x Word V d x 0 < d
122 pfxsuff1eqwrdeq d Word V x 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 Word V x 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 Word V x 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 Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 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 Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 lastS d = lastS x d = x
131 130 exp31 d Word V d = N + 2 d prefix N + 1 = W lastS W lastS d E x Word V x = N + 2 x prefix N + 1 = W lastS W lastS x E N 0 lastS d = lastS x d = x
132 22 30 131 syl2anb d D x D N 0 lastS d = lastS x d = x
133 132 impcom N 0 d D x D lastS d = lastS x d = x
134 14 133 sylbid N 0 d D x D F d = F x d = x
135 134 ralrimivva N 0 d D x D F d = F x d = x
136 dff13 F : D 1-1 R F : D R d D x D F d = F x d = x
137 6 135 136 sylanbrc N 0 F : D 1-1 R