Metamath Proof Explorer

Theorem efgred

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the terminal point. (Contributed by Mario Carneiro, 28-Sep-2015)

Ref Expression
Hypotheses efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
efgred.d ⊢ D = W ∖ ⋃ x ∈ W ran ⁡ T ⁡ x
efgred.s ⊢ S = m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟼ m ⁡ m − 1
Assertion efgred ⊢ A ∈ dom ⁡ S ∧ B ∈ dom ⁡ S ∧ S ⁡ A = S ⁡ B → A ⁡ 0 = B ⁡ 0

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
2 efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
3 efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
4 efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
5 efgred.d ⊢ D = W ∖ ⋃ x ∈ W ran ⁡ T ⁡ x
6 efgred.s ⊢ S = m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟼ m ⁡ m − 1
7 fviss ⊢ I ⁡ Word I × 2 𝑜 ⊆ Word I × 2 𝑜
8 1 7 eqsstri ⊢ W ⊆ Word I × 2 𝑜
9 1 2 3 4 5 6 efgsf ⊢ S : t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟶ W
10 9 fdmi ⊢ dom ⁡ S = t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1
11 10 feq2i ⊢ S : dom ⁡ S ⟶ W ↔ S : t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟶ W
12 9 11 mpbir ⊢ S : dom ⁡ S ⟶ W
13 12 ffvelrni ⊢ A ∈ dom ⁡ S → S ⁡ A ∈ W
14 13 adantr ⊢ A ∈ dom ⁡ S ∧ B ∈ dom ⁡ S → S ⁡ A ∈ W
15 8 14 sselid ⊢ A ∈ dom ⁡ S ∧ B ∈ dom ⁡ S → S ⁡ A ∈ Word I × 2 𝑜
16 lencl ⊢ S ⁡ A ∈ Word I × 2 𝑜 → S ⁡ A ∈ ℕ 0
17 15 16 syl ⊢ A ∈ dom ⁡ S ∧ B ∈ dom ⁡ S → S ⁡ A ∈ ℕ 0
18 peano2nn0 ⊢ S ⁡ A ∈ ℕ 0 → S ⁡ A + 1 ∈ ℕ 0
19 17 18 syl ⊢ A ∈ dom ⁡ S ∧ B ∈ dom ⁡ S → S ⁡ A + 1 ∈ ℕ 0
20 breq2 ⊢ c = 0 → S ⁡ a < c ↔ S ⁡ a < 0
21 20 imbi1d ⊢ c = 0 → S ⁡ a < c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ S ⁡ a < 0 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
22 21 2ralbidv ⊢ c = 0 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < 0 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
23 breq2 ⊢ c = i → S ⁡ a < c ↔ S ⁡ a < i
24 23 imbi1d ⊢ c = i → S ⁡ a < c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
25 24 2ralbidv ⊢ c = i → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
26 breq2 ⊢ c = i + 1 → S ⁡ a < c ↔ S ⁡ a < i + 1
27 26 imbi1d ⊢ c = i + 1 → S ⁡ a < c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ S ⁡ a < i + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
28 27 2ralbidv ⊢ c = i + 1 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
29 breq2 ⊢ c = S ⁡ A + 1 → S ⁡ a < c ↔ S ⁡ a < S ⁡ A + 1
30 29 imbi1d ⊢ c = S ⁡ A + 1 → S ⁡ a < c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ S ⁡ a < S ⁡ A + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
31 30 2ralbidv ⊢ c = S ⁡ A + 1 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ A + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
32 12 ffvelrni ⊢ a ∈ dom ⁡ S → S ⁡ a ∈ W
33 8 32 sselid ⊢ a ∈ dom ⁡ S → S ⁡ a ∈ Word I × 2 𝑜
34 lencl ⊢ S ⁡ a ∈ Word I × 2 𝑜 → S ⁡ a ∈ ℕ 0
35 33 34 syl ⊢ a ∈ dom ⁡ S → S ⁡ a ∈ ℕ 0
36 nn0nlt0 ⊢ S ⁡ a ∈ ℕ 0 → ¬ S ⁡ a < 0
37 35 36 syl ⊢ a ∈ dom ⁡ S → ¬ S ⁡ a < 0
38 37 pm2.21d ⊢ a ∈ dom ⁡ S → S ⁡ a < 0 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
39 38 adantr ⊢ a ∈ dom ⁡ S ∧ b ∈ dom ⁡ S → S ⁡ a < 0 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
40 39 rgen2 ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < 0 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
41 simpl1 ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d ∧ ¬ c ⁡ 0 = d ⁡ 0 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
42 simpl3l ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d ∧ ¬ c ⁡ 0 = d ⁡ 0 → S ⁡ c = i
43 breq2 ⊢ S ⁡ c = i → S ⁡ a < S ⁡ c ↔ S ⁡ a < i
44 43 imbi1d ⊢ S ⁡ c = i → S ⁡ a < S ⁡ c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
45 44 2ralbidv ⊢ S ⁡ c = i → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
46 42 45 syl ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d ∧ ¬ c ⁡ 0 = d ⁡ 0 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
47 41 46 mpbird ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d ∧ ¬ c ⁡ 0 = d ⁡ 0 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ c → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
48 simpl2l ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d ∧ ¬ c ⁡ 0 = d ⁡ 0 → c ∈ dom ⁡ S
49 simpl2r ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d ∧ ¬ c ⁡ 0 = d ⁡ 0 → d ∈ dom ⁡ S
50 simpl3r ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d ∧ ¬ c ⁡ 0 = d ⁡ 0 → S ⁡ c = S ⁡ d
51 simpr ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d ∧ ¬ c ⁡ 0 = d ⁡ 0 → ¬ c ⁡ 0 = d ⁡ 0
52 1 2 3 4 5 6 47 48 49 50 51 efgredlem ⊢ ¬ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d ∧ ¬ c ⁡ 0 = d ⁡ 0
53 iman ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d → c ⁡ 0 = d ⁡ 0 ↔ ¬ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d ∧ ¬ c ⁡ 0 = d ⁡ 0
54 52 53 mpbir ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S ∧ S ⁡ c = i ∧ S ⁡ c = S ⁡ d → c ⁡ 0 = d ⁡ 0
55 54 3expia ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S → S ⁡ c = i ∧ S ⁡ c = S ⁡ d → c ⁡ 0 = d ⁡ 0
56 55 expd ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ c ∈ dom ⁡ S ∧ d ∈ dom ⁡ S → S ⁡ c = i → S ⁡ c = S ⁡ d → c ⁡ 0 = d ⁡ 0
57 56 ralrimivva ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 → ∀ c ∈ dom ⁡ S ∀ d ∈ dom ⁡ S S ⁡ c = i → S ⁡ c = S ⁡ d → c ⁡ 0 = d ⁡ 0
58 2fveq3 ⊢ c = a → S ⁡ c = S ⁡ a
59 58 eqeq1d ⊢ c = a → S ⁡ c = i ↔ S ⁡ a = i
60 fveqeq2 ⊢ c = a → S ⁡ c = S ⁡ d ↔ S ⁡ a = S ⁡ d
61 fveq1 ⊢ c = a → c ⁡ 0 = a ⁡ 0
62 61 eqeq1d ⊢ c = a → c ⁡ 0 = d ⁡ 0 ↔ a ⁡ 0 = d ⁡ 0
63 60 62 imbi12d ⊢ c = a → S ⁡ c = S ⁡ d → c ⁡ 0 = d ⁡ 0 ↔ S ⁡ a = S ⁡ d → a ⁡ 0 = d ⁡ 0
64 59 63 imbi12d ⊢ c = a → S ⁡ c = i → S ⁡ c = S ⁡ d → c ⁡ 0 = d ⁡ 0 ↔ S ⁡ a = i → S ⁡ a = S ⁡ d → a ⁡ 0 = d ⁡ 0
65 fveq2 ⊢ d = b → S ⁡ d = S ⁡ b
66 65 eqeq2d ⊢ d = b → S ⁡ a = S ⁡ d ↔ S ⁡ a = S ⁡ b
67 fveq1 ⊢ d = b → d ⁡ 0 = b ⁡ 0
68 67 eqeq2d ⊢ d = b → a ⁡ 0 = d ⁡ 0 ↔ a ⁡ 0 = b ⁡ 0
69 66 68 imbi12d ⊢ d = b → S ⁡ a = S ⁡ d → a ⁡ 0 = d ⁡ 0 ↔ S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
70 69 imbi2d ⊢ d = b → S ⁡ a = i → S ⁡ a = S ⁡ d → a ⁡ 0 = d ⁡ 0 ↔ S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
71 64 70 cbvral2vw ⊢ ∀ c ∈ dom ⁡ S ∀ d ∈ dom ⁡ S S ⁡ c = i → S ⁡ c = S ⁡ d → c ⁡ 0 = d ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
72 57 71 sylib ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
73 72 ancli ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
74 35 adantr ⊢ a ∈ dom ⁡ S ∧ b ∈ dom ⁡ S → S ⁡ a ∈ ℕ 0
75 nn0leltp1 ⊢ S ⁡ a ∈ ℕ 0 ∧ i ∈ ℕ 0 → S ⁡ a ≤ i ↔ S ⁡ a < i + 1
76 nn0re ⊢ S ⁡ a ∈ ℕ 0 → S ⁡ a ∈ ℝ
77 nn0re ⊢ i ∈ ℕ 0 → i ∈ ℝ
78 leloe ⊢ S ⁡ a ∈ ℝ ∧ i ∈ ℝ → S ⁡ a ≤ i ↔ S ⁡ a < i ∨ S ⁡ a = i
79 76 77 78 syl2an ⊢ S ⁡ a ∈ ℕ 0 ∧ i ∈ ℕ 0 → S ⁡ a ≤ i ↔ S ⁡ a < i ∨ S ⁡ a = i
80 75 79 bitr3d ⊢ S ⁡ a ∈ ℕ 0 ∧ i ∈ ℕ 0 → S ⁡ a < i + 1 ↔ S ⁡ a < i ∨ S ⁡ a = i
81 80 ancoms ⊢ i ∈ ℕ 0 ∧ S ⁡ a ∈ ℕ 0 → S ⁡ a < i + 1 ↔ S ⁡ a < i ∨ S ⁡ a = i
82 74 81 sylan2 ⊢ i ∈ ℕ 0 ∧ a ∈ dom ⁡ S ∧ b ∈ dom ⁡ S → S ⁡ a < i + 1 ↔ S ⁡ a < i ∨ S ⁡ a = i
83 82 imbi1d ⊢ i ∈ ℕ 0 ∧ a ∈ dom ⁡ S ∧ b ∈ dom ⁡ S → S ⁡ a < i + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ S ⁡ a < i ∨ S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
84 jaob ⊢ S ⁡ a < i ∨ S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
85 83 84 bitrdi ⊢ i ∈ ℕ 0 ∧ a ∈ dom ⁡ S ∧ b ∈ dom ⁡ S → S ⁡ a < i + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
86 85 2ralbidva ⊢ i ∈ ℕ 0 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
87 r19.26-2 ⊢ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
88 86 87 bitrdi ⊢ i ∈ ℕ 0 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ∧ ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a = i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
89 73 88 syl5ibr ⊢ i ∈ ℕ 0 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < i + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
90 22 25 28 31 40 89 nn0ind ⊢ S ⁡ A + 1 ∈ ℕ 0 → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ A + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
91 19 90 syl ⊢ A ∈ dom ⁡ S ∧ B ∈ dom ⁡ S → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ A + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
92 17 nn0red ⊢ A ∈ dom ⁡ S ∧ B ∈ dom ⁡ S → S ⁡ A ∈ ℝ
93 92 ltp1d ⊢ A ∈ dom ⁡ S ∧ B ∈ dom ⁡ S → S ⁡ A < S ⁡ A + 1
94 2fveq3 ⊢ a = A → S ⁡ a = S ⁡ A
95 94 breq1d ⊢ a = A → S ⁡ a < S ⁡ A + 1 ↔ S ⁡ A < S ⁡ A + 1
96 fveqeq2 ⊢ a = A → S ⁡ a = S ⁡ b ↔ S ⁡ A = S ⁡ b
97 fveq1 ⊢ a = A → a ⁡ 0 = A ⁡ 0
98 97 eqeq1d ⊢ a = A → a ⁡ 0 = b ⁡ 0 ↔ A ⁡ 0 = b ⁡ 0
99 96 98 imbi12d ⊢ a = A → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ S ⁡ A = S ⁡ b → A ⁡ 0 = b ⁡ 0
100 95 99 imbi12d ⊢ a = A → S ⁡ a < S ⁡ A + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 ↔ S ⁡ A < S ⁡ A + 1 → S ⁡ A = S ⁡ b → A ⁡ 0 = b ⁡ 0
101 fveq2 ⊢ b = B → S ⁡ b = S ⁡ B
102 101 eqeq2d ⊢ b = B → S ⁡ A = S ⁡ b ↔ S ⁡ A = S ⁡ B
103 fveq1 ⊢ b = B → b ⁡ 0 = B ⁡ 0
104 103 eqeq2d ⊢ b = B → A ⁡ 0 = b ⁡ 0 ↔ A ⁡ 0 = B ⁡ 0
105 102 104 imbi12d ⊢ b = B → S ⁡ A = S ⁡ b → A ⁡ 0 = b ⁡ 0 ↔ S ⁡ A = S ⁡ B → A ⁡ 0 = B ⁡ 0
106 105 imbi2d ⊢ b = B → S ⁡ A < S ⁡ A + 1 → S ⁡ A = S ⁡ b → A ⁡ 0 = b ⁡ 0 ↔ S ⁡ A < S ⁡ A + 1 → S ⁡ A = S ⁡ B → A ⁡ 0 = B ⁡ 0
107 100 106 rspc2v ⊢ A ∈ dom ⁡ S ∧ B ∈ dom ⁡ S → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ A + 1 → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0 → S ⁡ A < S ⁡ A + 1 → S ⁡ A = S ⁡ B → A ⁡ 0 = B ⁡ 0
108 91 93 107 mp2d ⊢ A ∈ dom ⁡ S ∧ B ∈ dom ⁡ S → S ⁡ A = S ⁡ B → A ⁡ 0 = B ⁡ 0
109 108 3impia ⊢ A ∈ dom ⁡ S ∧ B ∈ dom ⁡ S ∧ S ⁡ A = S ⁡ B → A ⁡ 0 = B ⁡ 0