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∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
wwlksnextbij0.r ⊢R=n∈V|lastS⁡Wn∈E
wwlksnextbij0.f ⊢F=t∈D⟼lastS⁡t
Assertion wwlksnextinj ⊢N∈ℕ0→F:D⟶1-1R

Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v ⊢V=Vtx⁡G
2 wwlksnextbij0.e ⊢E=Edg⁡G
3 wwlksnextbij0.d ⊢D=w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
4 wwlksnextbij0.r ⊢R=n∈V|lastS⁡Wn∈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→wprefixN+1=dprefixN+1
17 16 eqeq1d ⊢w=d→wprefixN+1=W↔dprefixN+1=W
18 fveq2 ⊢w=d→lastS⁡w=lastS⁡d
19 18 preq2d ⊢w=d→lastS⁡WlastS⁡w=lastS⁡WlastS⁡d
20 19 eleq1d ⊢w=d→lastS⁡WlastS⁡w∈E↔lastS⁡WlastS⁡d∈E
21 15 17 20 3anbi123d ⊢w=d→w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E↔d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E
22 21 3 elrab2 ⊢d∈D↔d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E
23 fveqeq2 ⊢w=x→w=N+2↔x=N+2
24 oveq1 ⊢w=x→wprefixN+1=xprefixN+1
25 24 eqeq1d ⊢w=x→wprefixN+1=W↔xprefixN+1=W
26 fveq2 ⊢w=x→lastS⁡w=lastS⁡x
27 26 preq2d ⊢w=x→lastS⁡WlastS⁡w=lastS⁡WlastS⁡x
28 27 eleq1d ⊢w=x→lastS⁡WlastS⁡w∈E↔lastS⁡WlastS⁡x∈E
29 23 25 28 3anbi123d ⊢w=x→w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E↔x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E
30 29 3 elrab2 ⊢x∈D↔x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡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∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→d=N+2→d=x
34 33 adantl ⊢x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→d=N+2→d=x
35 34 com12 ⊢d=N+2→x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→d=x
36 35 3ad2ant1 ⊢d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E→x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→d=x
37 36 adantl ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E→x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→d=x
38 37 imp ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→d=x
39 38 adantr ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E∧N∈ℕ0→d=x
40 39 adantr ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E∧N∈ℕ0∧lastS⁡d=lastS⁡x→d=x
41 simpr ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E∧N∈ℕ0∧lastS⁡d=lastS⁡x→lastS⁡d=lastS⁡x
42 eqtr3 ⊢dprefixN+1=W∧xprefixN+1=W→dprefixN+1=xprefixN+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→dprefixN+1=dprefixd−1
57 oveq2 ⊢N+1=d−1→xprefixN+1=xprefixd−1
58 56 57 eqeq12d ⊢N+1=d−1→dprefixN+1=xprefixN+1↔dprefixd−1=xprefixd−1
59 55 58 syl ⊢N∈ℕ0∧d=N+2→dprefixN+1=xprefixN+1↔dprefixd−1=xprefixd−1
60 59 biimpd ⊢N∈ℕ0∧d=N+2→dprefixN+1=xprefixN+1→dprefixd−1=xprefixd−1
61 60 ex ⊢N∈ℕ0→d=N+2→dprefixN+1=xprefixN+1→dprefixd−1=xprefixd−1
62 61 com13 ⊢dprefixN+1=xprefixN+1→d=N+2→N∈ℕ0→dprefixd−1=xprefixd−1
63 42 62 syl ⊢dprefixN+1=W∧xprefixN+1=W→d=N+2→N∈ℕ0→dprefixd−1=xprefixd−1
64 63 ex ⊢dprefixN+1=W→xprefixN+1=W→d=N+2→N∈ℕ0→dprefixd−1=xprefixd−1
65 64 com23 ⊢dprefixN+1=W→d=N+2→xprefixN+1=W→N∈ℕ0→dprefixd−1=xprefixd−1
66 65 impcom ⊢d=N+2∧dprefixN+1=W→xprefixN+1=W→N∈ℕ0→dprefixd−1=xprefixd−1
67 66 com12 ⊢xprefixN+1=W→d=N+2∧dprefixN+1=W→N∈ℕ0→dprefixd−1=xprefixd−1
68 67 3ad2ant2 ⊢x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→d=N+2∧dprefixN+1=W→N∈ℕ0→dprefixd−1=xprefixd−1
69 68 adantl ⊢x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→d=N+2∧dprefixN+1=W→N∈ℕ0→dprefixd−1=xprefixd−1
70 69 com12 ⊢d=N+2∧dprefixN+1=W→x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→N∈ℕ0→dprefixd−1=xprefixd−1
71 70 3adant3 ⊢d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E→x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→N∈ℕ0→dprefixd−1=xprefixd−1
72 71 adantl ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E→x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→N∈ℕ0→dprefixd−1=xprefixd−1
73 72 imp31 ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E∧N∈ℕ0→dprefixd−1=xprefixd−1
74 73 adantr ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E∧N∈ℕ0∧lastS⁡d=lastS⁡x→dprefixd−1=xprefixd−1
75 simpl ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E→d∈WordV
76 simpl ⊢x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→x∈WordV
77 75 76 anim12i ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→d∈WordV∧x∈WordV
78 77 adantr ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E∧N∈ℕ0→d∈WordV∧x∈WordV
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∈WordV∧0<d→d≠∅
91 89 90 sylan2 ⊢d∈WordV∧d=N+2∧N∈ℕ0→d≠∅
92 91 exp32 ⊢d∈WordV→d=N+2→N∈ℕ0→d≠∅
93 92 com12 ⊢d=N+2→d∈WordV→N∈ℕ0→d≠∅
94 93 3ad2ant1 ⊢d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E→d∈WordV→N∈ℕ0→d≠∅
95 94 impcom ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E→N∈ℕ0→d≠∅
96 95 adantr ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→N∈ℕ0→d≠∅
97 96 imp ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡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∈WordV∧0<x→x≠∅
103 101 102 sylan2 ⊢x∈WordV∧x=N+2∧N∈ℕ0→x≠∅
104 103 exp32 ⊢x∈WordV→x=N+2→N∈ℕ0→x≠∅
105 104 com12 ⊢x=N+2→x∈WordV→N∈ℕ0→x≠∅
106 105 3ad2ant1 ⊢x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→x∈WordV→N∈ℕ0→x≠∅
107 106 impcom ⊢x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→N∈ℕ0→x≠∅
108 107 adantl ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E→N∈ℕ0→x≠∅
109 108 imp ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E∧N∈ℕ0→x≠∅
110 78 97 109 jca32 ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E∧N∈ℕ0→d∈WordV∧x∈WordV∧d≠∅∧x≠∅
111 110 adantr ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E∧N∈ℕ0∧lastS⁡d=lastS⁡x→d∈WordV∧x∈WordV∧d≠∅∧x≠∅
112 simpl ⊢d∈WordV∧x∈WordV→d∈WordV
113 112 adantr ⊢d∈WordV∧x∈WordV∧d≠∅∧x≠∅→d∈WordV
114 simpr ⊢d∈WordV∧x∈WordV→x∈WordV
115 114 adantr ⊢d∈WordV∧x∈WordV∧d≠∅∧x≠∅→x∈WordV
116 hashneq0 ⊢d∈WordV→0<d↔d≠∅
117 116 biimprd ⊢d∈WordV→d≠∅→0<d
118 117 adantr ⊢d∈WordV∧x∈WordV→d≠∅→0<d
119 118 com12 ⊢d≠∅→d∈WordV∧x∈WordV→0<d
120 119 adantr ⊢d≠∅∧x≠∅→d∈WordV∧x∈WordV→0<d
121 120 impcom ⊢d∈WordV∧x∈WordV∧d≠∅∧x≠∅→0<d
122 pfxsuff1eqwrdeq ⊢d∈WordV∧x∈WordV∧0<d→d=x↔d=x∧dprefixd−1=xprefixd−1∧lastS⁡d=lastS⁡x
123 113 115 121 122 syl3anc ⊢d∈WordV∧x∈WordV∧d≠∅∧x≠∅→d=x↔d=x∧dprefixd−1=xprefixd−1∧lastS⁡d=lastS⁡x
124 ancom ⊢dprefixd−1=xprefixd−1∧lastS⁡d=lastS⁡x↔lastS⁡d=lastS⁡x∧dprefixd−1=xprefixd−1
125 124 anbi2i ⊢d=x∧dprefixd−1=xprefixd−1∧lastS⁡d=lastS⁡x↔d=x∧lastS⁡d=lastS⁡x∧dprefixd−1=xprefixd−1
126 3anass ⊢d=x∧lastS⁡d=lastS⁡x∧dprefixd−1=xprefixd−1↔d=x∧lastS⁡d=lastS⁡x∧dprefixd−1=xprefixd−1
127 125 126 bitr4i ⊢d=x∧dprefixd−1=xprefixd−1∧lastS⁡d=lastS⁡x↔d=x∧lastS⁡d=lastS⁡x∧dprefixd−1=xprefixd−1
128 123 127 bitrdi ⊢d∈WordV∧x∈WordV∧d≠∅∧x≠∅→d=x↔d=x∧lastS⁡d=lastS⁡x∧dprefixd−1=xprefixd−1
129 111 128 syl ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E∧N∈ℕ0∧lastS⁡d=lastS⁡x→d=x↔d=x∧lastS⁡d=lastS⁡x∧dprefixd−1=xprefixd−1
130 40 41 74 129 mpbir3and ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡x∈E∧N∈ℕ0∧lastS⁡d=lastS⁡x→d=x
131 130 exp31 ⊢d∈WordV∧d=N+2∧dprefixN+1=W∧lastS⁡WlastS⁡d∈E∧x∈WordV∧x=N+2∧xprefixN+1=W∧lastS⁡WlastS⁡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∈DF⁡d=F⁡x→d=x
136 dff13 ⊢F:D⟶1-1R↔F:D⟶R∧∀d∈D∀x∈DF⁡d=F⁡x→d=x
137 6 135 136 sylanbrc ⊢N∈ℕ0→F:D⟶1-1R