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 syl6bb ⊢ 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